Protecting passwords is an important part of cyber security. Since at least the 1970s there has been a continuously escalating competition between those devising mechanisms to strengthen password protection and those devising methods to attack each new mechanism [Solar1].
Password files store associations between user names and encoded passwords. If a user X has a password Y then the password file will contain a representation of the pair (X, h(Y)), where h is a function, called a hash function, that is hard to invert. To check that X's password is Y, h(Y) is computed and the result compared with the hash stored in the password file. Password files are not strongly protected, so an attacker can easily obtain them, thus it is critical that knowledge of h(Y) does not easily lead to knowledge of Y. A naive brute-force attack is to pre-compute values of h(Y) where Y ranges over, say, all words in a dictionary. Then if one obtains h(Y) one can get the password Y by a comparison with precomputed hashes. The famous 1988 Morris worm cracked password files using essentially this method.
One way to make it harder to recover passwords from their hashes is to combine passwords with additional parameters before hashing them. If "||" denotes a combining operator (e.g. concatenation), then the password file will contain (X, h(P1||...||Pn||Y)) where P1,...,Pn are parameters, some of them perhaps randomly generated when the password Y is first entered (called a "salt"). Adding parameters before hashing makes it much harder to carry out brute-force attacks, since the precomputed set will be much larger as all parameter values need to be considered as well as values of Y. However, the parameters themselves have to be stored somewhere, and if an attacker can get hold of them then their security enhancing effect is nullified.
The project proposed here will investigate storing some secret parameters, and performing password hashing with them, in a physically separate hardware device. This has recently been advocated when strong password protection is required [Solar2]. We call our project "Mac in the Box" (MITB) after the HMAC cryptographic hash function based mechanism we plan to implement in our device [HMAC].
Our research aims to build both a password checking software application running on a server and a physically separate hardware device (plus software drivers) that can create password hashes using a parameter stored securely on the device. The hardware device will be simple, low cost, open source and formally verified to correctly implement a standard secure hash algorithm.
The primary research contribution of this project is the accurate end-to-end formal modelling of the specification and implementation of the hardware device and a machine checked proof that the implementation meets its specification. This will plug a gap in existing security arguments for storing hash parameters in separate hardware: for example the formal analysis of the Yubikey protocol by Kunnemann and Steel [YubiSecure] assumes "that the implementation is correct with respect to the documentation" [Solar2, Slide 9].
Our goal is that the device could be manufactured commercially and anyone could provide support or suitable wrappers for PHP, Java, Apache etc.
The research proposed here may appear very narrowly focused, but we see it as a first proof of concept for possibly many such projects where simple, low cost, open source and verified hardware devices provide a clear, easy to understand and use API that accomplishes essential tasks for internet security.
The project is a collaboration between a group with experience in high-level modelling of hardware security modules (HSMs) and using formal methods to find vulnerabilities in them (Steel/Inria) and a group experienced in high assurance software and hardware verification (Gordon/Cambridge).
Our approach aims to protect against malicious server software (or an attacker taking control). Although we will aim to create a working application and device drivers on the server, we will produce security arguments that maintaining password secrecy will not depend on this software being correct, so it will not need to be verified. The security of our password protection will depend on the correctness of the hardware, and it is this that will be formally verified.
Exactly how much and in what detail we need to model the hardware is part of the research. We hope to avoid having to verify the gate level implementations of communication devices (e.g. USB hardware), but this needs investigation. We will, however, formally verify the main software stack that implements the storage of secrets and the computation of hashes. This is described in more detail below. We do not aim to make our hardware prototypes tamper-resistant, nor to attempt to protect against TEMPEST or other side channels. The verification will just focus on functional correctness.
The documentation level specification will also define the effects of hardware or communication errors (e.g. if the device fails to sync with a server, loses power etc.). It is expected that in such cases an error state will result, from which, after a reset (either automatic or via user intervention), the normal ready state will be entered.
The programming platform will extend a functional language core with features suitable for implementing low-level operating system (OS) facilities such as device drivers, handling hardware exceptions (e.g. loss of power), memory management (both volatile and non-volatile) and, possibly, crypto co-processor thread management.
It is hoped that the platform implemented for this project will have general applicability as a new way to create small very high assurance hardware-software applications. The MITB example will demonstrate this, but there are other examples that could be the focus of future projects; for example, general security tokens, electronic fuses, locks and keys, and payment authorisation dongles.
As described earlier, a central research goal is plugging the gap in existing security arguments for storing hash parameters in a separate hardware device, like YubiKey.
To achieve this, our aim is to certify by machine checked mathematical proof, that the low-level bytecode implementation of MITB correctly implements the high level formal documentation, including both normal and error behavior. A separate verification will certify implementations of the bytecode with respect to the implementation method used (ARM processor or FPGA).
It is possible we may use proof-certified synthesis to create some parts of the implementation; other parts being certified by post hoc verification.
Cambridge has considerable historical and ongoing research experience in the specification and verification of hardware and low-level software which we hope to build upon. Examples of this include:
Inria has extensive experience in formal methods, security (including web security, protocols and hardware token APIs), applied cryptography and run-time analysis.
The MITB project aims to use the results emerging from this research and to demonstrate applications of it.
[Solar1] http://www.openwall.com/presentations/PHDays2012-Password-Security [Solar2] http://www.openwall.com/presentations/YaC2012-Password-Hashing-At-Scale [HMAC] http://www.ietf.org/rfc/rfc2104.txt [YubiSecure] http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KS-stm12.pdf [MyreenSynth] http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf [FoxARM] http://www.cl.cam.ac.uk/~acjf3/arm/ [GordonIyodaSynth] http://www.cl.cam.ac.uk/~mjcg/proposals/dev/ [ChoudaryGrobertMetz] http://eprint.iacr.org/2012/374 [LastPassYubiKey] http://helpdesk.lastpass.com/security-options/yubikey-authentication/