Confidential computing has proven its value in cloud environments, but its potential for securing edge and high-end embedded systems (e.g., automotive controllers, cryptographic accelerators, telco infrastructure) remains largely unexplored. We present ACE, an open-source, royalty-free virtualization-based confidential computing system for RISC-V targeting these environments. ACE isolates software into confidential virtual machines with narrow, well-defined interfaces, building exclusively on commodity RISC-V hardware without specialized hardware extensions or licensing fees. Our prototype evaluation on the first commercially available RISC-V hardware supporting virtualization shows that ACE is a viable candidate for our target systems.

Confidential computing is a key technology for isolating high-assurance applications from the large amounts of untrusted code typical in modern systems. Existing confidential computing systems cannot be certified for use in critical applications, like systems controlling critical infrastructure, hardware security modules, or aircraft, because they lack formal verification. This paper presents an approach to formally modeling and proving a security monitor for confidential computing. It introduces a canonical architecture for virtual machine (VM)-based confidential computing systems. It abstracts processor-specific components and identifies a minimal set of hardware primitives required by a trusted security monitor to enforce security guarantees. This paper focuses on verifying the software assuming a correct hardware implementation. We demonstrate our methodology and proposed approach with an example from our open-source Rust implementation of the security monitor for RISC-V.

This paper presents Protected Execution Facility (PEF), a virtual machine-based Trusted Execution Environment (TEE) for confidential computing on Power ISA. PEF enables protected secure virtual machines (SVMs). Like other TEEs, PEF verifies the SVM prior to execution. PEF utilizes a Trusted Platform Module (TPM), secure boot, and trusted boot as well as newly introduced architectural changes for Power ISA systems. Exploiting these architectural changes requires new firmware, the Protected Execution Ultravisor. PEF is supported in the latest version of the POWER9 chip. PEF demonstrates that access control for isolation and cryptography for confidentiality is an effective approach to confidential computing. We particularly focus on how our design (i) balances between access control and cryptography, (ii) maximizes the use of existing security components, and (iii) simplifies the management of the SVM life cycle. Finally, we evaluate the performance of SVMs in comparison to normal virtual machines on OpenPOWER systems.

Protecting the security and privacy of data is a paramount concern of enterprises in medical, educational, financial, and other highly regulated industries. While some industries have moved rapidly to take advantage of the cost savings, innovations in data analysis, and many benefits provided by cloud platforms, regulated enterprises with sensitive data have proceeded with caution. In this paper, we explore a fully public cloud-based architecture that is able to handle both service requirements and security requirements. In such a public cloud environment, the traditional notion of static perimeter-based reactive security can leave internal system components vulnerable to accidental data disclosures or malicious attacks originating from within the perimeter. Therefore, ensuring security and compliance of such a solution requires innovation and new approaches in several directions, including proactive log monitoring and analysis of virtually all parts of the cloud-based solution, full end-to-end data encryption from the client through Internet transmission to data storage and analytics in the solution, and robust firewall and network-intrusion detection systems. We discuss many of these techniques as applied to a specific real-world application known as the Watson Genomic Analytics Prototype.

This article features lessons learned in designing, developing, and testing features for a high-assurance smart card operating system. In particular, this paper describes software design, development, and testing process, and the advantages reaped from following established process guidelines. The authors describe the project impact experienced from external influences and count among them market pressure from a rapidly changing commercial landscape which demands agility in order to assure continued funding and product success.

This paper describes the design of the random number generator (RNG) in the Caernarvon high assurance smart card operating system. Since it is used in the generation of cryptographic keys and other sensitive materials, the RNG has a number of stringent security requirements that the random bits must be of good quality i.e. the bits must not be predictable or biased. To this end, a number of standards such as the German AIS 31 mandate that true random bits be continuously tested before use in sensitive applications such as key generation. A key issue in implementing this standard is that such testing before use in key generation greatly increases the attack surface for side-channel attacks. For example, template attacks which can extract information about the random bits from even a single run provided we use the same bits at many different points in the computation. Because of these potential risks, the Caernarvon operating system uses pseudo random number generators which are initially seeded by externally generated high quality random bits, and then perturbed by bits from the true random number generator. We describe a PRNG design which yields high quality random bits while also ensuring that it is not susceptible to side-channel attacks and provide an informal argument about its effectiveness.

Paul Karger, a great friend to all and a thought leader in security, passed away in September 2010.

Building a high-assurance, secure operating system for memory constrained systems, such as smart cards, introduces many challenges. The increasing power of smart cards has made their use feasible in applications such as electronic passports, military and public sector identification cards, and cell-phone based financial and entertainment applications. Such applications require a secure environment, which can only be provided with sufficient hardware and a secure operating system. We argue that smart cards pose additional security challenges when compared to traditional computer platforms. We discuss our design for a secure smart card operating system, named Caernarvon, and show that it addresses these challenges, which include secure application download, protection of cryptographic functions from malicious applications, resolution of covert channels, and assurance of both security and data integrity in the face of arbitrary power losses.

The ever-increasing computational power of smart cards has made them feasible for applications like electronic passports and military id cards. However, these applications require a secure smart card operating system. In this paper we argue that smart card platforms pose additional security challenges than traditional computer platforms. We discuss our design for a secure smart card operating system, called Caernarvon, and show it addresses these challenges, such as secure application download, protecting cryptographic functions from potentially malicious applications, resolving covert channel issues, assuring both security and data integrity in the face of arbitrary power losses, etc.

In this paper, we describe results of a case study to establish the feasibility of deriving mappings between an abstract user level specification and the code elements in a concrete implementation of a highly secure smart card operating system. Such a mapping is necessary for feedback-directed specification-based test generation to improve code coverage, needed by the stringent criteria for high-assurance systems. We used test cases generated from the user level specification to identify the executed code elements and attempted to use static analysis to map the unexecuted code elements to the corresponding elements in the user level specification. Our primary result is evidence that, given a sufficiently expressive user level specification and a test generation system that is able to effectively use such a specification, the resulting tests will cover the vast majority of the code branches that are able to be covered. Therefore, the benefit of a feedback-directed system will be limited. We further provide evidence that the static analysis required to generate feedback in these cases tends to be difficult, involving inferring the semantics of the internal implementation of data structures. In particular, we observed that the internal states at the implementation level in a high security application pose significant challenges to this mapping process.

In this paper, we describe results of two case studies designed to satisfy the testing requirements mandated by higher levels of the Common Criteria for security evaluations. These requirements include 1) Demonstrable independence of individual test cases 2) Demonstrable coverage of both user level specifications and implementation code. The case studies are based on a highly secure smart card operating system. In the first case study, we used automated specification based test generation, together with fault injection, to demonstrate that self-contained test cases are independent and do not lead to fault masking. The goal of the second case study was to demonstrate adequate code coverage, while retaining the ability to generate expected outputs based on specifications. To that end, we first established mappings between the specification and implementation code elements. Test cases were then generated from the user level specification to identify the executed code elements and we attempted to use static analysis to map the unexecuted code elements to the corresponding elements in the user level specification. In this second case study, we found that, given a sufficiently expressive user level specification, and a test generation system that is able to effectively use such a specification, the resulting tests will cover the vast majority of the code branches that are able to be covered. Therefore, the benefit of a feedback-directed system will be limited. We further provide evidence that the static analysis required to generate feedback in these cases tends to be difficult, involving inferring the semantics of the internal implementation of data structures. In particular, we observed that the internal states at the implementation level in a high security application pose significant challenges to this mapping process.

The Caernarvon operating system was developed to demonstrate that a high assurance system for smart cards was technically feasible and commercially viable. The entire system has been designed to be evaluated under the Common Criteria at EAL7, the highest defined level of assurance. Historically, smart card processors have not supported the hardware protection features necessary to separate the OS from the applications, and one application from another. The Caernarvon OS has taken advantage of the first smart card processors with such features to be the first smart card OS to provide this kind of protection. Even when compared with conventional systems where the hardware protection is routine, the Caernarvon OS is noteworthy, because of the EAL7 assurance. This approach facilitated implementation of a formally specified, mandatory security policy providing multi-level security (MLS) suitable for both government agencies and commercial users. The mandatory security policy requires effective authentication of its users that is independent of applications. For this reason, the Caernarvon OS also contains a privacy-preserving, two-way authentication protocol integrated with the Mandatory Security Policy. The Caernarvon OS includes a strong cryptographic library that has been separately certified under the Common Criteria at EAL5+ for use with other systems. The Caernarvon OS implements a secure method for downloading trusted and untrusted application software and data in the field, with the assumption that all applications are potentially hostile. While the initial platform for the operating system was smart cards, the design could also be used in other embedded devices, such as USB tokens, PDAs, cell phones, etc.

Unsecure computational environments threaten many financial cryptography implementations, and other sensitive computation. High-performance secure coprocessors can address these threats. However, using this technology for practical security solutions requires overcoming numerous technical and business obstacles. These obstacles motivate building a high-performance secure coprocessor that balances security with easy third-party programmability—but these obstacles also provide many design challenges. This paper discusses some of issues we faced when attempting to build such a device.