PassCert﹕Exploring the Impact of Formal Verification on the Adoption of Password Security Software
With the explosive growth of our data economy, the quantity of personal data and other valuable assets available online has increased massively. At the same time, despite years of searching for viable alternatives, text passwords remain the dominant access control mechanism to access that data and those assets.
Users’ attitudes towards passwords can thus put at risk the security of our data economy. For example, users have shown that they tend to choose weak passwords that are easy to guess by password cracking software. Moreover, many users reuse the same password across different systems, which can have serious consequences for users and organizations affected by data breaches. In the last few years, breaches at organizations like Yahoo!, Dropbox, Lastpass, LinkedIn, and eBay have exposed over a billion user passwords to attackers.
To address this problem, security experts recommend the use of password managers (PMs) that combine secure password storage and retrieval with random password generation. These tools can improve account security by enabling the use of strong and unique passwords, simultaneously improving the usability and convenience of text password authentication. However, despite its critical importance, the adoption of PMs is still low. Reasons for this include distrust on the storage mechanisms and on the quality of generated passwords.
PassCert’s short-term vision is to build an open-source, proof-of-concept PM that through the use of formal verification, is guaranteed to satisfy properties on data storage and password generation. The goal is to help non-expert users to use stronger passwords without sacrificing convenience, whilst conveying the formal guarantees in an effective way. We aim to determine whether formal verification can increase users’ confidence in PMs and thus increase their adoption. The proof-of-concept PM will result from a close collaboration between researchers from INESC-ID Lisboa, INESC TEC, and The Carnegie Mellon CyLab Security and Privacy Institute.
Contacts
Principal Investigator in Portugal: João F. Ferreira
Principal Investigator at CMU: Nicolas Christin
Participant institutions:
- INESC-ID: Instituto de Engenharia de Sistemas e Computadores, Investigação e Desenvolvimento em Lisboa (INESC-ID)
- Instituto Superior Técnico, Universidade de Lisboa
- INESC TEC: Instituto de Engenharia de Sistemas e Computadores, Tecnologia e Ciência
- School of Computer Science, Carnegie Mellon University
- CyLab: Carnegie Mellon University Security and Privacy Institute
Funding
PassCert is a CMU Portugal Exploratory Research Project that is funded by the Fundação para a Ciência e a Tecnologia (FCT).