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.

This article presents a novel intrinsic image transfer (IIT) algorithm for image illumination manipulation, which creates a local image translation between two illumination surfaces. This model is built on an optimization-based framework composed of illumination, reflectance and content photo-realistic losses, respectively. Each loss is first defined on the corresponding sub-layers factorized by an intrinsic image decomposition and then reduced under the well-known spatial-varying illumination illumination-invariant reflectance prior knowledge. We illustrate that all losses, with the aid of an "exemplar" image, can be directly defined on images without the necessity of taking an intrinsic image decomposition, thereby giving a closed-form solution to image illumination manipulation. We also demonstrate its versatility and benefits to several illumination-related tasks: illumination compensation, image enhancement and tone mapping, and high dynamic range (HDR) image compression, and show their high-quality results on natural image datasets.

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.

Spinlocks have been widely used as a solution for synchronous accesses to shared resources, and their correctness is critical to guarantee the consistency of concurrent processes. This paper presents formal models and machine-checked verification of the correctness of spinlocks at instruction level. We present the formal verification of two spinlocks, which are spinlocks implemented based on the ARM instructions and the x86 instructions, respectively. Our model formalizes the lowlevel instructions that are necessary to capture the execution of spinlocks, characterizes the processor hardware mechanisms related to each instruction, and considers the context switches on processors and two-level scheduling of processors and processes. We specify the correctness property of our models, that is, accesses of a critical section satisfy mutual exclusion, and verify that the models satisfy the property using the theorem prover Isabelle/HOL. With the verification experience, we give some suggestions on how to implement spinlock leveraging the ARM ISA.

Secure enclaves provide a practical solution to secure computation, and current approaches to secure enclaves are implemented by extending hardware security mechanisms to the CPU architecture. Therefore, it is hard for a platform to offer secure computation if its CPU architecture is not equipped with any secure enclave features. Unfortunately, ARM CPUs, dominating mobile devices and having increasing momentum in cloud markets, do not provide any security mechanisms achieving the security equivalent to modern secure enclave architectures. In this paper, we propose SecTEE, a software-based secure enclave architecture which is based on the CPU's isolation mechanism and does not require specialized security hardware of the CPU architecture such as memory encryption engines. SecTEE achieves a high level of security even compared with hardware-based secure enclave architectures: resistance to privileged host software attacks, lightweight physical attacks, and memory access based side-channel attacks. Besides, SecTEE provides rich trusted computing primitives for enclaves: integrity measurement, remote attestation, data sealing, secrets provisioning, and life cycle management. We implement a SecTEE prototype based on the ARM TrustZone technology, but our approach can be applied to other CPU architectures with isolation mechanisms. The evaluation results show that most overhead comes from the software encryption and the runtime overhead imposed by trusted computing primitives is acceptable.

The development of the Internet of Things has made embedded devices widely used. Embedded devices are often used to process sensitive data, making them the target of attackers. ARM TrustZone technology is used to protect embedded device data from compromised operating systems and applications. But as the value of the data stored in embedded devices increases, more and more effective physical attacks have emerged. However, TrustZone cannot resist physical attacks. We propose SoftME, an approach that utilizes the on-chip memory space to provide a trusted execution environment for sensitive applications. We protect the confidentiality and integrity of the data stored on the off-chip memory. In addition, we design task scheduling in the encryption process. We implement a prototype system of our approach on the development board supporting TrustZone and evaluate the overhead of our approach. The experimental results show that our approach improves the security of the system, and there is no significant increase in system overhead.

Abstract The new released trusted platform module (TPM) specification, TPM2.0, adds cryptographic support for key exchange by providing SM2 authenticated key exchange (AKE) application programming interface (API) commands. Xu analyzed the SM2 AKE protocol and found that it was insecure in common computing environment by presenting two types of unknown key share attacks. Here, we present another design weakness of the SM2 AKE protocol, which might cause that the protocol cannot be proven secure in modern security models. We also analyze the security of SM2 AKE protocol in TPM2.0, whose running environment is very different and find that (i) it indeed gets some security improvements through the protection capability provided by the two SM2 AKE commands of TPM2.0 but (ii) it still has some weaknesses, which might lead to unknown key share and key‐compromise impersonation attacks because of the bad design of the TPM2.0 application programming interface. We solve the weaknesses of SM2 AKE protocol in TPM2.0 by slightly modifying one SM2 AKE command and finally give a formal proof of our solution in the Canetti and Krawczyk model. Our work shows that TPM2.0 could provide a proven secure SM2 AKE by slightly modifying one command. Copyright © 2014 John Wiley & Sons, Ltd.

The binary attestation mechanism is a basic remote attestation way for Trusted Platform Module (TPM) in Trusted Computing Group (TCG) specification. To improve the security and complexity of the binary attestation, the concept of property-based attestation (PBA) has been proposed by convincing the remote verifier that the platform satisfies the security properties without exposure of the configuration privacy. The existing PBA schemes have the disadvantage of the complex property revocations. To overcome this problem, we propose a simplified property based attestation model on the online TTP in this paper. During the attestation the prover attests the platform configuration property as well as the validation of the property certificate without verifying the property revocation. More concretely it presents a property based attestation protocol with variable privacy, which is provable security under the q-SDH assumption, discrete logarithm problem and the perfect hidden property of the commitment. We conduct the experiment to evaluate efficiency of our scheme in final. The experiment shows that the privacy parameter does not have the significant impacts on the performance, and we can adjust the parameter to make a trade-off between the performance and privacy.