Hardware supply-chain attacks are raising significant security threats to the boot process of multiprocessor systems. In this paper, we investigate critical stages of the multiprocessor system boot process and identify a new, prevalent hardware supply-chain attack surface that can bypass secure boot due to the absence of processor-authentication mechanisms. To defend against such attacks, in this paper, we present PA-Boot, the first formally verified processor-authentication protocol for secure boot in multiprocessor systems. PA-Boot is proved functionally correct and is guaranteed to detect multiple adversarial behaviors, such as processor replacements and man-in-the-middle attacks. The fine-grained formalization of PA-Boot and its fully mechanized security proofs are carried out in the Isabelle/HOL theorem prover with 348 lemmas/theorems and ~7,100 LoC. We further implement in C an instance of PA-Boot. Experiments on the proof-of-concept implementation indicate that PA-Boot can effectively identify boot-process attacks with a minor overhead (4.98% on Linux boot process) and thereby improve the security of multiprocessor systems.

We present the first formal semantics for the Solana eBPF bytecode language used in smart contracts on the Solana blockchain platform. Our formalization accurately captures all binary-level instructions of the Solana eBPF instruction set architecture. This semantics is structured in a small-step style, facilitating the formalization of the Solana eBPF interpreter within Isabelle/HOL. We provide a semantics validation framework that extracts an executable semantics from our formalization to test against the original implementation of the Solana eBPF interpreter. This approach introduces a novel lightweight and non-invasive method to relax the limitations of the existing Isabelle/HOL extraction mechanism. Furthermore, we illustrate potential applications of our semantics in the formalization of the main components of the Solana eBPF virtual machine

The Trusted Execution Environment (TEE) plays a crucial role in modern computer systems and the compromise of TEE can result in enormous losses. Although numerous TEE products have been proposed, most of them lack robust security guarantees. To address this concern, GlobalPlatform (GP) defines the TEE security standard, Protection Profile (PP), which has gained widespread adoption in the TEE development and Common Criteria (CC) evaluation. However, despite its importance, GPTEE PP has never been formally specified and verified. In this paper, we present ProveriT , a parameterized, composable, and formally verified model of GPTEE PP. Firstly, we propose the first formal specification of GPTEE PP in a parameterized manner, encompassing the definition of security problems, security objectives, and security functional requirements. Secondly, we provide a compositional framework, utilizing horizontal calculus and vertical calculus, to flexibly combine specific security functional requirements for TEE developers and reduce proof efforts for verification. ProveriT is extensible and reusable for the verification and CC evaluation of specific TEE products. Thirdly, we conduct a comprehensive formal verification of rationales in the model to ensure the correctness of GPTEE PP. During the verification, 8 issues are discovered and we provide suggestions to resolve them. Finally, we demonstrate the extensibility and effectiveness of ProveriT by applying it to the verification of a commercial TEE. All the specifications and verification are carried out in the Isabelle/HOL theorem prover.

Virtual Private Cloud (VPC) has become a widely used cloud computing service, serving as a foundational web infrastructure for many organizations. Nevertheless, the growing problem of reachability issues poses significant threats to the security and reliability of VPC networks, potentially resulting in critical security concerns such as data breaches and service outages. Although there has been substantial progress in recent reachability analysis, existing methods lack validation of correctness. Moreover, current analyses are tailored for One-to-One reachability where both the source and the destination are fixed, and fail to efficiently answer One-to-Multi reachability queries, which involve computing all reachable destinations for a given source node. To address the above challenges, we propose VeriReach, the first formally verified algorithm that provides comprehensive and efficient reachability analysis in large-scale VPC networks. The reachability analysis result of VeriReach is proved to be equivalent to the original reachability semantics of the VPC networks, ensuring its correctness (i.e., soundness and completeness). The fine-grained formalization of VeriReach and its fully mechanized correctness proofs are carried out in Isabelle/HOL theorem prover with 282 lemmas/theorems and $\sim 4,900{\mathrm{LoC}}$. We further implement VeriReach in C++ and the evaluations indicate that VeriReach is more efficient and scalable than MonoSAT, the state-of-the-art SMT solver, when applied to large-scale VPC networks for reachability analysis.

Trusted Execution Environments (TEEs) play a crucial role in embedded systems, IoT, and cloud computing. However, their security issues are a major concern, particularly related to defects or improper implementations in access control mechanisms. Such issues can result in severe problems like privilege escalation and unintended memory accesses during inter-domain communication. Moreover, employing mathematical methods for rigorous security guarantees is essential.To address these challenges, we propose Lark, a cross-domain access control for TEEs, which is modeled and verified in Isabelle/HOL. Lark applies orthogonal access control attributes on memory to decouple access permissions of different privilege levels. Additionally, it enforces strict access permission checks for inter-domain communications. For a strict security guarantee, Lark is formalized and verified in Isabelle/HOL, with 84 definitions and 35 lemmas containing ∼1,600 lines of code. The machine-checkable proofs demonstrate that Lark ensures memory isolation and information flow security. We identify and resolve an inter-domain communication issue within an open-source TEE, and develop a prototype that implements the access control features of Lark. Exhaustive evaluations on real-world applications demonstrate that Lark introduces less than 5% performance overhead.