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

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2017

Autores

Ferreira, JF (Autor) Outra; Johnson, SA (Autor) Outra; Mendes, A (Autor) Outra; Brooke, PJ (Autor) Outra

Ata de Conferência Internacional

Título: Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings

Páginas: 407-421

13th International Conference on Integrated Formal Methods, IFM 2017

20 September 2017 through 22 September 2017

Indexação

Scopus - 3 Citações

Outras Informações

ID Authenticus: P-00N-PGS

DOI: 10.1007/978-3-319-66845-1_27

Abstract (EN): 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. © Springer International Publishing AG 2017.

Idioma: Inglês

Tipo (Avaliação Docente): Científica