Complex safety-critical systems require multiple models for a comprehensive description, resulting in error-prone development and laborious verification. Bidirectional transformation (BX) is an approach to automatically synchronizing these models. However, existing BX frameworks lack formal verification to enforce these models’ consistency rigorously. This paper introduces KBX, a formal bidirectional transformation framework for verified model synchronization. First, we present a matching logic-based BX model, providing a logical foundation for constructing BX definitions within the \(\mathbb{K}\) framework. Second, we propose algorithms to synthesize formal BX definitions from unidirectional ones, which allows developers to focus on crafting the unidirectional definitions while disregarding the reverse direction and missing information recovery for synchronization. Afterward, we harness \(\mathbb{K}\) to generate a formal synchronizer from the synthesized definitions for consistency maintenance and verification. To evaluate the effectiveness of KBX, we conduct a comparative analysis against existing BX frameworks. Furthermore, we demonstrate the application of KBX in constructing a BX between UML and HCSP for real-world scenarios, showcasing an 72% reduction in BX development effort compared to manual specification writing in \(\mathbb{K}\) .

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.

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.

The challenge of requirements for the finer-grained isolated domain in Trusted Execution Environment (TEE) has been increasing, including the accuracy and security of resource management. However, the current access control mechanism for TEE cannot provide strict security assurances due to a lack of strict formal verification. In order to address the problem, in this paper, we first present the definition of multi-domain TEE, and propose a verified tag-based access control framework called REAL to provide the strict access control policy. We develop a high-level formal functional specification of REAL, and prove its correctness and security properties with 119 lemmas/theorems and ∼ 4,000 LOC of Isabelle/HOL. We also implement a page-level access control prototype called SOP-TEE and demonstrate that it correctly achieve the security objectives while merely incurring less than 0.3% overhead.