Certified Password Quality: A Case Study Using Coq and Linux Pluggable Authentication Modules


We propose the use of modern proof assistants to specify, implement, and verify password quality checkers. We use the proof assistant Coq, focusing on Linux PAM, a widely-used implementation of pluggable authentication modules for Linux. We show how password quality policies can be expressed in Coq and how to use Coq’s code extraction features to automatically encode these policies as PAM modules that can readily be used by any Linux system. We implemented the default password quality policy shared by two widely-used PAM modules: pam cracklib and pam pwquality. We then compared our implementation with the original modules by running them against a random sample of 100,000 leaked passwords obtained from a publicly available database. In doing this, we demonstrated a potentially serious bug in the original modules. The bug was reported to the maintainers of Linux PAM and is now fixed.

In 13th International Conference on integrated Formal Methods (iFM 2017)
Alexandra Mendes
Assistant Professor

My research focuses on innovative user interfaces for formal methods and mathematical approaches to software quality. More recently, I started work on usable security, in particular on the impact of formal verification on the use and adoption of formally verified security software product. Much of my most recent work overlaps with the area of software engineering. I am also interested on innovative and fun ways to teach Computer Science. For more details, see selected publications and some of my projects. Follow me on Twitter or add me on LinkedIn.