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}\) .

Concurrent wireless charging offers significant performance improvements for Wireless Rechargeable Sensor Networks (WRSNs). However, wave interference, arising from interactions between electromagnetic waves from multiple chargers, disrupts this process. This results in uneven power distribution, potentially leading to significantly attenuated or even negligible energy reception at certain locations. This paper addresses this challenge by introducing the Concurrent cHarging with Efficient phaSe Scheduling (CHESS) problem. CHESS maximizes the energy received by critical sensors through a novel on-demand phase scheduling approach. To achieve this, we propose a practical charging model with charger phases and wave interference effects. Subsequently, a charger grouping algorithm reduces computational complexity, followed by a phase vector searching algorithm to identify optimal phases for maximizing sensor energy reception. Finally, a phase scheduling algorithm enables dynamic adaptation to the evolving energy demands. Simulations show significant efficiency improvements, outperforming baseline algorithms by an average of ${8 9. 8 \%}$

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.

Sensitive resources in Trusted Execution Environment (TEE) have suffered serious security threats in recent years. Previous protection approaches either lack a strong assurance of TEE security properties or are limited to a single platform. We propose a compatible verified TEE architecture, calledCVTEE, which delegates a security monitor to manage TEE resources securely. This architecture has two key advantages: i) its functional correctness and security are guaranteed by a machine-checkable proof of security objectives of Trusted Application (TA) isolation, runtime confidentiality, and runtime integrity, and ii) it is applicable to different TEE platforms and implementation-independent due to its high level of abstraction and non-determinism of data types. Note that access control policy and information flow control policy are the core for security management of resources. After formally specifying the security attributes of TEE resources, we develop these policies based on Common Criteria (CC) in the security monitor and provide atomic interfaces.CVTEEis formally verified with 386 lemmas/theorems and$\sim$10,000 LOC of Isabelle/HOL. In addition, we implement a proof of concept for the access control module of Teaclave, and prove that the constructed access control model meets the security requirements through 5 theorems.