The "Mac in the Box" (MITB) project (named after HMAC) aims to design, formally verify and build a simple, low cost, open source hardware device for hashing passwords and other data.
The goal of the MITB project is to explore plugging a gap in existing security arguments for storing hash parameters in separate hardware: for example the formal analysis of the Yubikey protocol by Künnemann and Steel assumes "that the implementation is correct with respect to the documentation" (see Slide 9 here). Eventually it is planned to build both a hashing application running on a server and the physically separate MITB hardware device to create password hashes using parameters stored securely on the device.
The project was conceived at the 2011 FMATS workshop where Graham Steel gave a talk showing that the APIs of many crypto tokens were badly designed and had unexpected insecurities that could be automatically found using his Tookan tool (this work, in turn, built on earlier research by Clulow, Bond and others). To complement research on breaking existing tokens, Graham and Mike conceived a research project to see how easy would it be to design new token implementations that were feasible to formally verify to have security properties establishing their trustworthiness (in particular, to be unbreakable using Tookan-like tools). The project aims to combine the API cracking expertise of Steel's group at INRIA with the verification expertise of Cambridge. Initially an ambitious project to verify a full PKCS #11 token was planned. This goal evolved into the much less ambitious MITB project, which aims to be a proof-of-concept first step.