SEASHIP

Challenge

Increasingly, cryptographic functions such as digital signatures and encryption are fundamental to protecting digital assets. To make those functions accessible in a uniform and manageable way, many enterprises use Hardware Security Modules (HSMs) that provide a consistent interface and encapsulation of both those primitives and the cryptographic keys on which they rely.

Today, HSMs are typically scarce, centralized resources only accessible via an organization's network, creating several risks: first, network-dependent connectivity puts at risk the confidentiality of sensitive data as it moves to and from HSMs; second, centralization puts availability at risk if HSMs fail or are subject to denial of service attacks; third, HSM resources scale out of band with other computing resources, making it difficult to meet dynamically changing needs. An additional challenge in the current approach is that current practice ignores the life cycle of provisioning HSMs, leading to potentially compromised equipment long before its deployment to a specific use. 

Solution

In the Secure and Efficient Automatically Secure Hardware IP (SEASHIP) Project, Galois’s name for its contribution to the Defense Advanced Research Projects Agency (DARPA)’s Automatic Implementation of Secure Silicon (AISS) Program, Galois is taking a Rigorous Digital Engineering (RDE) approach to show that centralized HSMs can be replaced by similar functionality that overcomes the challenges above by deployment as a distributed, decentralized resource included in every System on Chip (SoC) acquired by an organization. 

RDE encompasses a model-based systems engineering (MBSE) methodology, infused with the rigor of formal methods, and equipped with a set of integrated analysis tools that can precisely and accurately reason about requirements and systems architectures, as well as both software and hardware implementations. At each step in the systems engineering process, RDE facilitates traceability and mechanized analysis with mathematical precision. With SEASHIP, Galois is using a combination of automated RDE tools, cryptographic engineering and proofs, and traditional ASIC design techniques to create a “soft IP” HSM that can be included in an ASIC design and automatically configured at design time to select which cryptographic functions to include. 

Following our RDE methodology, we begin by creating a functional and lifecycle specification, including minimum security requirements. We then create a rapidly configurable, top-level hardware design using domain-specific programming languages for system architecture and workflow definition. Our tools can generate security engine product line alternatives as needed – all in line with the specification. Finally, we simulate and validate the resulting implementation(s) using software test harnesses (automatically generated from the specification) to generate evidence that each design (implementation) matches designer intent (specification).

Correct- and Secure-by-Construction

At each step of this process, Galois’s combined RDE and Advanced Cryptography approach ensures that the end product is both correct- and secure-by-construction.

While typical engineering design ignores operational security or cryptographic IP in order to “get to market” quickly, or uses ad hoc security design rules of thumb that result in vulnerabilities that are only discovered after that IP has moved to production, SEASHIP uses a combination of sound cryptographic threat modeling and security proofs; proven side-channel resilience; and automatic test generation to demonstrate that cryptographic services can be operationally secure by design, preventing both direct and side-channel vulnerabilities.

In addition, SEASHIP explicitly includes auditable protocols for provisioning throughout the HSM cycle. Cryptographic and identity assets provisioned during the manufacturing process are used to control and authorize asset provisioning later, when the manufactured devices are integrated into systems, deployed to user organizations, and further provisioned by those organizations. Protocols for re-purposing SEASHIP HSMs assure that re-deployment and re-provisioning can be accomplished without revealing former assets or risking device compromise. Finally, end-of-life transitions are explicit in SEASHIP, so that devices that may no longer be reliable cannot be re-deployed or re-used in the future. At all points in the life cycle, asset accessibility is positively controlled to assure full life cycle security.

The Result

Our automated RDE system facilitates the automatic generation of a collection of security engines and their assurance as evidence. The result is a configurable Silicon Security Engine (SE) capability, with rigorous cryptographic security proofs, demonstrated side-channel resilience, positively controlled life cycle transitions, and automatic thorough testing, that can be embedded in any SoC design prior to manufacturing, to provide cryptographic services for on-device functions. 

Value Add

• SE designs with diverse cryptographic capabilities automatically configured by user-chosen parameters, with automatically generated tests to provide evidence and assure correctness
• Explicit, auditable security across all stages of device life cycle, from manufacturing to integration to repeated deployment and use, and including end-of-life security
• Improved system performance
• Improved resilience to power side-channel attacks and direct exploitation of the SE’s interface