Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

The ACL2 model used for the FIPS level 4 evaluation of the IBM 4758 secure coprocessor

The IBM 4758 was the first device ever to achieve the highest certification level (4) for cryptographic devices, according to Federal Information Processing Standards (FIPS) 140-1; it is (to date) the only device to have achieved level 4 for both hardware and software. Conventional computers are not physically protected, so those that process confidential data must be kept a controlled environment (something like a guarded room) to shield them from physical attack; in contrast, the 4758 (which is about the size of a thick book) has withstood all known physical attacks (except perhaps by the military), so it can be used to safely store confidential data unguarded in a hostile environment. Furthermore, the 4758 provides a mechanism that allows software to be securely downloaded over insecure channels (such as the internet). These characteristics make this device especially attractive for e-commerce applications. As part of the software evaluation, a formal model of the code responsible for downloading software was written and several properties concerning the model were proved. In my talk I will describe the 4758, the FIPS requirements concerning formal modelling, and the ACL2 model that satisfied these requirements.

Vernon Austel