Biblio

Mobile embedded terminals widely applied in individual lives, but its security threats become more and more serious. Malicious attacker can steal sensitive information such as user’s phonebook, credit card information by instrumenting malicious programs, or compromising vulnerable software. Against these problems, this paper proposes a scheme for trusted protection system on the embedded platform. The system uses SM algorithms and hardware security chip as the root of trust to establish security mechanisms, including trusted boot of system image, trusted monitoring of the system running environment, disk partition encryption and verification, etc. These security mechanisms provide comprehensive protection to embedded system boot, runtime and long-term storage devices. This paper introduces the architecture and principles of the system software, design system security functions and implement prototype system for protection of embedded OS. The experiments results indicates the promotion of embedded system security and the performance test shows that encryption performance can meet the practical application.

In recent years, the rapid development of virtualization and container technology brings unprecedented impact on traditional IT architecture. Trusted Computing devotes to provide a solution to protect the integrity of the target platform and introduces a virtual TPM to adapt to the challenges that virtualization brings. However, the traditional integrity measurement solution and remote attestation has limitations due to the challenges such as large of measurement and attestation cost and overexposure of configurations details. In this paper, we propose the Partial Attestation Model. The basic idea of Partial Attestation Model is to reconstruct the Chain of Trust by dividing them into several separated ones. Our model therefore enables the challenger to attest the specified security requirements of the target platform, instead of acquiring and verifying the complete detailed configurations. By ignoring components not related to the target requirements, our model reduces the attestation costs. In addition, we further implement an attestation protocol to prevent overexposure of the target platform's configuration details. We build a use case to illustrate the implementation of our model, and the evaluations on our prototype show that our model achieves better efficiency than the existing remote attestation scheme.

In this paper, we present a formal model for the verification of the DNSsec Protocol in the interactive theorem prover Isabelle/HOL. Relying on the inductive approach to security protocol verification, this formal analysis provides a more expressive representation than the widely accepted model checking analysis. Our mechanized model allows to represent the protocol, all its possible traces and the attacker and his knowledge. The fine grained model allows to show origin authentication, and replay attack prevention. Most prominently, we succeed in expressing Delegation Signatures and proving their authenticity formally.