The project PassCert – Exploring the Impact of Formal Verification on the Adoption of Password Security Software, started in February and will allow the creation of a password manager that ensures security properties on data storage and generation of passwords, using formal verification.
More specifically, the PassCert project aims to determine whether formal verification can increase the users’ confidence in password managers, thus increasing their adoption. The work developed within the scope of the project will favour the close collaboration between researchers from INESC TEC’s High-assurance Software Laboratory (HASLab), INESC-ID Lisbon and Carnegie Mellon University.
Computer security experts recommend using password managers that combine secure storage with the random generation of strong passwords. However, despite its critical importance, the adoption of password managers is still relatively low, partially due to a certain distrust in the storage mechanisms and the quality of the generated passwords. In this sense, the PassCert project represents “an important step towards increasing confidence in the use of these systems and their adoption, through formal guarantees on security properties and the way they are transmitted to users”, said Alexandra Mendes, researcher at HASLab.
The INESC TEC team, composed of Alexandra Mendes and José Bacelar Almeida, is involved in the entire project, but is mainly focused on the verification and usability tasks, as well as on the verification of the cryptographic components necessary to the development of the password manager.
The INESC TEC researchers mentioned in this news piece are associated with UBI and UMinho.