Trusting Trusted hardware:
Towards a Formal Model for Programmable Secure Coprocessors

Sean W. Smith and Vernon Austel
IBM T. J. Watson Research Center

- hardware for full certification at FIPS 140-1 level 4

Generic Secure Coprocessor

Generic secure coprocessor is formed by: Physical tamper causes zeroing the memory.

FLASH contains several layers:


System Configuration

The system configuration is a tuple of relevant properties: Valid configuration = a configuration that can be reached from a valid configuration through a series of valid transitions
Necessary trust set = those parties who, if they abuse or distribute their secrets, can make it impossible for B to make this distinction

Correctness for architecture components