Abstract

This paper describes the design of an integrated high assurance separation kernel and a Secret Protected (SP) hardware for cryptographic services. Integrating SP with the separation kernel requires (1) augmenting the SP instruction set with additional hardware instructions to aid virtualization and ensure that the confidentiality of user's secrets are protected to the same extent as in the original design of SP (2) augmenting the separation kernel to ensure minimization of information flow via covert channels resulting from integration of SP (3) reconciling the user specific model and the usage model of the integrated design and (4) controlling flow of information about user's secrets across the different Secrecy, and Integrity labels. The architecture called Secure Core, is designed for networked mobile devices to be used by a single user at a time. We define usage scenarios in which users may need to assume different roles, that translate into different security profiles for the user. We begin with a description of the separation kernel and the SP architecture. This is followed by a description of the hardware requirements for virtualization of SP integration and use of the virtualized cryptographic SP services. We find that the main changes required to SP are the ability to save and restore SP state as the SecureCore kernel switches between virtual machines, so that isolation properties are maintained when using SP. We conclude with a security analysis, including the effect of the virtualization and integration on the confidentiality/integrity of user secrets as well as enforcement of MAC on user secrets like cryptographic keys. The integration of SP hardware …

Date

January 1, 1970

Authors

Ganesha Bhaskara, Timothy E Levin, Thuy D Nguyen, Cynthia E Irvine, Terry V Benzel, Jeffrey S Dwoskin, Ruby B Lee

Publisher

Technical report, Princeton University Department of Electrical Engineering Technical Report CE-L2006-006