Abstract An OS microkernel can be extended by implementing services upon it. A service could introduce an object that references a kernel object, and implement a group of functions that invokes the functions for manipulating the kernel object. We consider the scenario where the microkernel has been verified with machine-checkable proofs, while the services remain to be verified. Moreover, the verification of the microkernel is not performed with the verification of subsequent extension in mind. We address the problem of how to build sufficiently on the verification results for the microkernel, in achieving the verification of the services. Our methodology consists of enhancements to the verification framework for the microkernel, and the design of invariants for establishing the connection between the service-level objects and the kernel-level objects. Using the methodology, we have conducted a substantial formal verification of a group of services extending the inter-task communication functionalities of the preemptive microkernel $$\mu \!\!\text{ C }\!\!\text{/ }\!\!\!\text{ OS-II }$$ μ C / OS-II . Our verification uncovers dormant bugs and provides a level of correctness assurance for the services that is above what is achievable through extensive testing.

ARM TrustZone is a hardware security technology commonly used to implement the Trusted Execution Environment (TEE), which is a hardware-based isolated execution environment in which security-critical software can execute without interference and is widely applied to embedded systems. Isolation of interrupts in the two security domains of TrustZone is an important security mechanism that plays a vital role in protecting the execution of the TEE. This paper introduces a formal modeling and verification approach for the interrupt isolation mechanism of the TEE based on TrustZone. We propose a model formalizing the TrustZone-based TEE system at the instruction level, which focuses on modeling system behaviors of interrupt handling and captures crucial instructions related to interrupt isolation. We formally define three types of properties for the model: correctness, safety, and information flow security. The verification results in the theorem prover Isabelle/HOL show that the model satisfies the above properties, which indicates that the interrupt isolation mechanism of TrustZone correctly enforces the isolation of interrupts and protects the TEE from being interfered with non-secure interrupts.

The trusted execution environment (TEE) is the security basis of embedded systems, which can provide a hardware-based isolated execution environment for security-sensitive components. Isolation of memory is a critical mechanism of TEE, the security of which plays a very important role in TEE's construction. In this paper, we present a formal verification of security properties about the memory isolation mechanism of TEE systems based on the ARM TrustZone, which is a hardware security technology commonly used on billions of ARM processors to create TEE. We establish a formal model of memory isolation, which consists of the formalization of ARMv8 architecture hardware components related to memory isolation and the formalization of a TrustZone monitor supporting world switch. We formally explicit and verify the correctness properties of memory management along with the information flow security properties of the memory isolation mechanism. The formalizations and verifications are all performed in the interactive theorem prover Isabelle/HOL.

Abstract Camera pose estimation is key to the proper functioning of robotic systems, supporting critical tasks such as robot navigation, target tracking, camera calibration, etc.Whilemultiple algorithms solving this problem have been proposed, their correctness has rarely been validated using formal techniques. This is true despite the fact that the adoption of formal verification is essential for the reliability of safety-critical systems, and for their certification to high assurance levels. In this article, we present an effort in formally verifying an algorithm for camera pose estimation in an interactive theorem prover. The algorithm leverages the power of Rodrigues formula to solve the pose estimation problem under conditions for which existing solutions cannot be applied. The technical ingredients include (but are not limited to) mechanized proofs of the Rodrigues formula (along with its Cayley decomposition form) and the least squares method for fitting data. Based on the formalization of the algorithm, we formally derive and verify its general solution and unique solution.

The differential of matrix functions(DMF) plays an important role in mathematics and engineering. Common applications of it are found in optimization analysis, computer vision, robotics, etc. In this paper, a formal method based on HOL is used to construct the DMF based on Fréchet differential in matrix space. In order to illustrate the practical effectiveness of our work, we use our formalization to verify a property of matrix exponential.