We propose and demonstrate SPIDER4TianoCore, a packaged Python command-line tool that provides integration-stage patch-status evidence for the TianoCore/UEFI firmware supply chain. Given an upstream pre-patch and post-patch pair and prepared downstream targets, the tool reports Vulnerable, Already Patched, Not Applicable, or Uncertain with supporting evidence for maintainer review. Our work is inspired by SPIDER's patch-propagation framing, but SPIDER4TianoCore does not itself prove that a patch is safe to propagate. We evaluate the engine on 20 prepared target/CVE pairs from eight public downstream EDK II repositories and two CVEs. The analyzers produce 10 high-confidence pre-patch matches and four high-confidence post-patch matches, conservatively abstain on six targets, and make no confidently wrong classifications relative to the recorded manual patch-state labels. These preliminary results demonstrate reproducible evidence generation for prepared targets rather than general downstream accuracy.

Bootloaders are present in every device, from IoT and edge devices to datacenter servers, making them critical to system security. Modern platforms establish hardware root of trust via vendor-specific mechanisms such as CPU microcode and authenticated code modules before bootloader execution. This SoK focuses on the software boot chain that follows that hardware-rooted integrity handoff. Prior work has focused on subsets of bootloaders, often using inconsistent terminology, leaving gaps in understanding their structure and interactions. We analyze 43 bootloaders and categorize them into three types based on their architecture and role in the boot process. We define attack surfaces for each type using our open-source dataset, BOOTBENCH, which includes 3,658 vulnerabilities and associated commits. Leveraging BOOTBENCH, we evaluate existing vulnerability detection techniques and highlight open problems, and examine limitations in defensive techniques for hardening bootloaders.

Memory-safety errors remain a persistent source of zero-day vulnerabilities in low-level software. The problem is especially acute in embedded systems, where hardware protections are often limited and dynamic analysis is difficult to apply effectively. Memory-safety verification can provide stronger assurance by proving the absence of such errors or exposing violations when they exist. However, current verification workflows remain largely manual and require substantial specialized expertise, limiting their adoption in practice. We present AutoSOUP, a system for automating component-level memory-safety verification through Safety-Oriented Unit Proofs. We formalize these unit proofs as artifacts that encode verification choices (scope, loop bounds, and environment models) for verifying safety properties, and introduce three techniques for deriving them automatically. To overcome the limitations of existing automation approaches, we further introduce LLM-As-Function-Call, a hybrid architecture that combines deterministic program synthesis with LLMs to automate these techniques and produce justifiable unit proofs. We evaluate AutoSOUP by assessing its ability to automate memory-safety verification and expose vulnerabilities in verified components, and we characterize the assumptions and guarantees of the resulting proofs.

Autonomous systems that offload computation to distributed edge, cloud, or volunteer nodes face a fundamental runtime resilience problem: verifying results from untrusted workers is costly and unreliable under Byzantine behavior, especially when adversaries adapt to evade detection. Existing approaches such as fixed replication incur constant overhead, while simpler auditing schemes fail to eliminate strategic adversaries. We propose DisTrust, a self-adaptive trust-based verification mechanism that dynamically redistributes work based on agent reliability, increasing scrutiny on suspicious nodes and progressively reducing their influence until they are ejected. The system requires no prior knowledge of the number or behavior of adversaries and naturally adjusts its verification effort to the observed threat level. We show that DisTrust suppresses and ejects gaming and omniscient Byzantine adversaries below the 50% threshold, while reducing verification overhead and avoiding the persistent damage and inefficiency of fixed replication baselines.

Security vulnerabilities in GitHub Actions are increasingly leading to software supply chain attacks. In some instances, attackers have modified a project's source code by crafting a malicious issue title. To mitigate such threats, GitHub introduced a permission system that allows project maintainers to customize the privilege granted to workflows and their jobs. Unfortunately, permission policy specification is a known hard problem across nearly all domains of computing, particularly when it is introduced after an ecosystem has been established. This paper proposes Cosseter, a static analysis tool designed to determine least-privilege permission policies for jobs within GitHub Actions workflow specifications. To achieve this goal, Cosseter overcomes state explosion challenges in static analysis of JavaScript Actions that result from packing and nuances in commonly used npm dependencies. We evaluated Cosseter using a dataset of manual permission annotations of JavaScript Actions used by industry tools and found that it has a comparable precision and recall. We further evaluate Cosseter at scale, studying the permission needs of 1,842 vulnerable workflows identified by prior work and extracting permission summaries for $\mathbf{8, 3 5 3}$ JavaScript Actions. We find that Cosseter's permission policy can reduce 76 % of 1,274 high severity code injection vulnerabilities into medium, low, or no severity. In doing so, we demonstrate how Cosseter suggested permissions can provide a valuable defense against software supply chain attacks.

Memory safety defects pose a major threat to software reliability, enabling cyberattacks, outages, and crashes. To mitigate these risks, organizations adopt Compositional Bounded Model Checking (BMC), using unit proofs to formally verify memory safety. However, methods for creating unit proofs vary across organizations and are inconsistent within the same project, leading to errors and missed defects. In addition, unit proofing remains understudied, with no systematic development methods or empirical evaluations. This work presents the first empirical study on unit proofing for memory safety verification. We introduce a systematic method for creating unit proofs that leverages verification feedback and objective criteria. Using this approach, we develop 73 unit proofs for four embedded operating systems and evaluate their effectiveness, characteristics, cost, and generalizability. Our results show unit proofs are cost-effective, detecting 74% of recreated defects, with an additional 9% found with increased BMC bounds, and 19 new defects exposed. We also found that embedded software requires small unit proofs, which can be developed in 87 minutes and executed in 61 minutes on average. These findings provide practical guidance for engineers and empirical data to inform tooling design.

Vendors are often provided with updated versions of a piece of software, fixing known security issues. However, the inability to have any guarantee that the provided patched software does not break the functionality of its original version often hinders patch deployment. This issue is particularly severe when the patched software is only provided in its compiled binary form. In this case, manual analysis of the patch's source code is impossible, and existing automated patch analysis techniques, which rely on source code, are not applicable. Even when the source code is accessible, the necessity of binary-level patch verification is still crucial, as highlighted by the recent XZ Utils backdoor. To tackle this issue, we propose VERIBIN, a system able to compare a binary with its patched version and determine whether the patch is "Safe to Apply", meaning it does not introduce any modification that could potentially break the functionality of the original binary. To achieve this goal, VERIBIN checks functional equivalence between the original and patched binaries. In particular, VERIBIN first uses symbolic execution to systematically identify patch-introduced modifications. Then, it checks if the detected patch-introduced modifications respect specific properties that guarantee they will not break the original binary ' s functionality. To work without source code, VERIBIN ' s design solves several challenges related to the absence of semantic information (removed during the compilation process) about the analyzed code and the complexity of symbolically executing large functions precisely. Our evaluation of VERIBIN on a dataset of 86 samples shows that it achieves an accuracy of 93.0% with no false positives, requiring only minimal analyst input. Additionally, we showcase how VERIBIN can be used to detect the recently discovered XZ Utils backdoor.

Modern computing systems remain rife with software vulnerabilities. Engineers apply many means to detect them, of which dynamic testing is one of the most common and effective. However, most dynamic testing techniques follow a top-down paradigm, and struggle to reach and exercise functions deep within the call graph. While recent works have proposed Bottom-Up approaches to address these limitations, they face challenges with false positives and generating valid inputs that adhere to the context of the entire program. In this work, we introduce a new paradigm that we call Reactive Bottom-Up Testing. Our insight is that function-level testing is necessary but not sufficient for the validation of vulnerabilities in functions. What we need is a systematic approach that not only tests functions in isolation but also validates their behavior within the broader program context, ensuring that detected vulnerabilities are both reachable and triggerable. We develop a three-stage bottom-up testing scheme: (1) identify likely-vulnerable functions and generate type- and context-aware harnesses; (2) fuzz to find crashes and extract input constraints via symbolic execution; (3) verify crashes by combining constraints to remove false positives. We implemented an automated prototype, which we call Griller. We evaluated Griller in a controlled setting using a benchmark of 48 known vulnerabilities across 5 open-source projects, where we successfully detected 28 known vulnerabilities. Additionally, we evaluated Griller on several real-world applications such as Pacman, and it discovered 6 previously unknown vulnerabilities. Our findings suggest that Reactive Bottom-Up Testing can significantly enhance the detection of vulnerabilities in complex systems, paving the way for more robust security practices.

We are increasingly relying on Internet of Things (IoT) devices for most of our daily tasks. However, IoT devices are riddled with security vulnerabilities. Most IoT devices have an associated Mobile Companion App (CApp) that enables users to control and access these devices remotely in a user-friendly manner. CApps are manufactured by the device vendors, and they trust these IoT devices. This blind trust results in DtM vulnerabilities, where attackers can compromise CApps by exploiting the corresponding IoT device. In this paper, we present RearFind, the first static analysis technique to find DtM vulnerabilities in CApps. We also design an interactive triaging technique to reduce false positive alerts through user feedback. Our evaluation shows that RearFind was able to find 5 new (i.e., previously unknown) DtM vulnerabilities. Our interactive triaging technique was able to reduce the false positives by 12%.

Third-party libraries like Log4j accelerate software application development but introduce substantial risk. Vulnerabilities in these libraries have led to Software Supply Chain (SSC) attacks that compromised resources within the host system. These attacks benefit from current application permissions approaches: thirdparty libraries are implicitly trusted in the application runtime. An application runtime designed with Zero-Trust Architecture (ZTA) principles secure access to resources, continuous monitoring, and least-privilege enforcement could mitigate SSC attacks, as it would give zero implicit trust to these libraries. However, no individual security defense incorporates these principles at a low runtime cost. This paper proposes Zero-Trust Dependencies to mitigate SSC vulnerabilities: we apply the NIST ZTA to software applications. First, we assess the expected effectiveness and configuration cost of Zero-Trust Dependencies using a study of third-party software libraries and their vulnerabilities. Then, we present a system design, ZTD_SYS, that enables the application of Zero-Trust Dependencies to software applications and a prototype, ZTD_JAVA, for Java applications. Finally, with evaluations on recreated vulnerabilities and realistic applications, we show that ZTD_JAVA can defend against prevalent vulnerability classes, introduces negligible cost, and is easy to configure and use.

Embedded software, predominantly written in C, is prone to memory corruption vulnerabilities due to spatial memory issues. Although various memory safety techniques exist, they are often unsuitable for embedded systems due to resource constraints and a lack of standardized OS support. Checked C, a backward-compatible, memory-safe C dialect, offers a potential solution by using pointer annotations for runtime checks to enhance spatial memory safety with minimal overhead. This paper provides the first experience report of porting EDK2 (an open-source UEFI implementation), an exemplary embedded codebase to Checked C, highlighting challenges and providing insights into applying Checked C to similar embedded systems. We also provide an enhanced automated annotation tool e3c, which improves the conversion rate by 25%, enabling easier conversion to Checked C.

Developers are increasingly integrating Language Models (LMs) into their mobile apps to provide features such as chat-based assistants. To prevent LM misuse, they impose various restrictions, including limits on the number of queries, input length, and allowed topics. However, if the LM integration is insecure, attackers can bypass these restrictions and gain unrestricted access to the LM, potentially harming developers' reputations and leading to significant financial losses. This paper presents the first systematic study of insecure usage of LMs by Android apps. We first manually analyze a preliminary dataset of apps to investigate LM integration methods, construct a taxonomy that categorizes the LM usage restrictions implemented by the apps, and determine how to bypass them. Alarmingly, we can bypass restrictions in 127 out of 181 apps. Then, we develop LM-Scout, a fully automated tool to detect on a large-scale vulnerable usage of LMs in 2,950 mobile apps. LM-Scout shows that, in many cases (i.e., 120 apps), it is possible to find and exploit such security issues automatically. Finally, we identify the root causes for the identified issues and offer recommendations for secure LM integration.

Embedded software is deployed in billions of devices worldwide, including in safety-sensitive systems like medical devices and autonomous vehicles. Defects in embedded software can have severe consequences. Many embedded software products incorporate Open-Source Embedded Software (EMBOSS), so it is important for EMBOSS engineers to use appropriate mechanisms to avoid defects. One of the common security practices is to use Static Application Security Testing (SAST) tools, which help identify commonly occurring vulnerabilities. Existing research related to SAST tools focuses mainly on regular (or non-embedded) software. There is a lack of knowledge about the use of SAST tools in embedded software. Furthermore, embedded software greatly differs from regular software in terms of semantics, software organization, coding practices, and build setup. All of these factors influence SAST tools and could potentially affect their usage. In this experience paper, we report on a large-scale empirical study of SAST in EMBOSS repositories. We collected a corpus of 258 of the most popular EMBOSS projects, and then measured their use of SAST tools via program analysis and a survey (N=25) of their developers. Advanced SAST tools are rarely used -- only 3% of projects go beyond trivial compiler analyses. Developers cited the perception of ineffectiveness and false positives as reasons for limited adoption. Motivated by this deficit, we applied the state-of-the-art (SOTA) CodeQL SAST tool and measured its ease of use and actual effectiveness. Across the 258 projects, CodeQL reported 709 true defects with a false positive rate of 34%. There were 535 (75%) likely security vulnerabilities, including in major projects maintained by Microsoft, Amazon, and the Apache Foundation. EMBOSS engineers have confirmed 376 (53%) of these defects, mainly by accepting our pull requests. Two CVEs were issued. Based on these results, we proposed pull requests to include our workflows as part of EMBOSS Continuous Integration (CI) pipelines, 37 (71% of active repositories) of these are already merged. In summary, we urge EMBOSS engineers to adopt the current generation of SAST tools, which offer low false positive rates and are effective at finding security-relevant defects.

Unified Extensible Firmware Interface (UEFI) specification describes a platform-independent pre-boot interface for an Operating System (OS). EDK-2 Vulnerabilities in UEFI interface functions have severe consequences and can lead to Bootkits and other persistent malware resilient to OS reinstallations. However, there exist no vulnerability detection techniques for UEFI interfaces. We present FUZZUER, a feedback-guided fuzzing technique for UEFI interfaces on EDK-2, an exemplary and prevalently used UEFI implementation. We designed FIRNESS that utilizes static analysis techniques to automatically generate fuzzing harnesses for interface functions. We evaluated FUZZUER on the latest version of EDK-2. Our comprehensive evaluation on 150 interface functions demonstrates that FUZZUER with FIRNESS is an effective testing technique of EDK-2's UEFI interface functions, greatly outperforming HBFA, an existing testing tool with manually written harnesses. We found 20 new security vulnerabilities, and most of these are already acknowledged by the developers.

As the adoption of wearable and smart devices increases, their privacy and security are still a concern. These devices collect sensitive data and constantly communicate with each other, posing new privacy threats that need to be understood and addressed. In this paper, we analyze the privacy of smart devices from a multi-device perspective. The central premise of our work is that information available at each device may be non-sensitive or lightly so, but by orchestrating information from multiple connected smart devices, it is possible to infer sensitive content. To verify this, we conduct a user study to understand user perceptions towards privacy on smart devices and contrast them with their actual behavior while operating these devices. We then present an attack framework that can leverage tightly coupled and connected smart devices, such as mobile, wearable, and smart TV, to leak sensitive information inferred from individually non-sensitive data. Finally, we introduce a tool based on NLP techniques to identify potential privacy vulnerabilities on smart devices and propose an integrated solution to increase smart devices' security. This analysis helps close the gap between user's perception and reality regarding privacy risks within their smart ecosystem.

Program partitioning is a proven technique for isolating potentially vulnerable code from trusted program components. We argue that an extreme isolation mechanism is not needed for all use cases. However, existing approaches tightly couple the security policy (what to partition) with the isolation mechanism (how to partition) making them inflexible. We propose TYPEFLEXER, which cleanly separates these concerns through a type-directed design. Our novel type system uses tainted annotations to mark entities that must be isolated, ensuring that tainted components do not interfere with untainted ones. To facilitate this process, we introduce TYPEMATIC, an automated annotation tool that not only propagates taint information according to our type rules but also identifies critical taint explosion points, allowing developers to apply explicit sanitizations where needed. We demonstrate the flexibility of our approach by designing three distinct isolation mechanisms, each with unique security guarantees and performance trade-offs. Our evaluation shows that TYPEFLEXER effectively contains vulnerabilities with negligible overhead as compared to the 12.8% performance penalty seen in existing state-of-the-art program partitioning techniques.

Federated Learning (FL) is a collaborative learning paradigm enabling participants to collectively train a shared machine learning model while preserving the privacy of their sensitive data. Nevertheless, the inherent decentralized and data-opaque characteristics of FL render its susceptibility to data poisoning attacks. These attacks introduce malformed or malicious inputs during local model training, subsequently influencing the global model and resulting in erroneous predictions. Current FL defense strategies against data poisoning attacks either involve a trade-off between accuracy and robustness or necessitate the presence of a uniformly distributed root dataset at the server. To overcome these limitations, we present FedZZ, which harnesses a zone-based deviating update (ZBDU) mechanism to effectively counter data poisoning attacks in FL. The ZBDU approach identifies the clusters of benign clients whose collective updates exhibit notable deviations from those of malicious clients engaged in data poisoning attack. Further, we introduce a precision-guided methodology that actively characterizes these client clusters (zones), which in turn aids in recognizing and discarding malicious updates at the server. Our evaluation of FedZZ across two widely recognized datasets: CIFAR10 and EMNIST, demonstrate its efficacy in mitigating data poisoning attacks, surpassing the performance of prevailing state-of-the-art methodologies in both single and multi-client attack scenarios and varying attack volumes. Notably, FedZZ also functions as a robust client selection strategy, even in highly non-IID and attack-free scenarios. Moreover, in the face of escalating poisoning rates, the model accuracy attained by FedZZ displays superior resilience compared to existing techniques. For instance, when confronted with a 50% presence of malicious clients, FedZZ sustains an accuracy of 67.43%, while the accuracy of the second-best solution, FL-Defender, diminishes to 43.36%.

Embedded software is used in safety-critical systems such as medical devices and autonomous vehicles, where software defects, including security vulnerabilities, have severe consequences. Most embedded codebases are developed in unsafe languages, specifically C/C++, and are riddled with memory safety vulnerabilities. To prevent such vulnerabilities, RUST, a performant memory-safe systems language, provides an optimal choice for developing embedded software. RUST interoperability enables developing RUST applications on top of existing C codebases. Despite this, even the most resourceful organizations continue to develop embedded software in C/C++. This paper performs the first systematic study to holistically understand the current state and challenges of using RUST for embedded systems. Our study is organized across three research questions. We collected a dataset of 2,836 RUST embedded software spanning various categories and 5 Static Application Security Testing ( SAST) tools. We performed a systematic analysis of our dataset and surveys with 225 developers to investigate our research questions. We found that existing RUST software support is inadequate, SAST tools cannot handle certain features of RUST embedded software, resulting in failures, and the prevalence of advanced types in existing RUST software makes it challenging to engineer interoperable code. In addition, we found various challenges faced by developers in using RUST for embedded systems development.

GitHub workflows or GitHub CI is a popular continuous integration platform that enables developers to automate various software engineering tasks by specifying them as workflows, i.e., YAML files with a list of jobs. However, engineering valid workflows is tedious. They are also prone to severe security issues, which can result in supply chain vulnerabilities. Recent advancements in Large Language Models (LLMs) have demonstrated their effectiveness in various software development tasks. However, GitHub workflows differ from regular programs in both structure and semantics. We perform the first comprehensive study to understand the effectiveness of LLMs on five workflow-related tasks with different levels of prompts. We curated a set of $\sim$400K workflows and generated prompts with varying detail. We also fine-tuned LLMs on GitHub workflow tasks. Our evaluation of three state-of-the-art LLMs and their fine-tuned variants revealed various interesting findings on the current effectiveness and drawbacks of LLMs.

Rust's high-performance memory safety features help eliminate an entire class of vulnerabilities, making it an attractive choice for mission-critical applications. Another important advantage of using Rust is the availability of a large number of libraries, i.e., crates, that make it easy to develop applications in Rust. However, crates need to be specially designed, i.e., no_std compatible, to be usable on embedded systems. Unfortunately, the majority of the crates are not no_std compatible. In this work, we tackle this problem by developing an automated code refactoring tool, Aunor, to specialize a given crate to be no_std compatible in a valid and backward compatible manner. Our preliminary evaluation shows Aunor is effective and could automatically convert 318 crates.