Formally Specifying and Verifying Linux-PAM Configurations Using Hierarchical Coloured Petri Nets and NuSMV

Abstract

<p>Authentication frameworks and their implementations are essential to securing computer systems and networks. One such framework is the Pluggable Authentication Modules (PAM) published in 1995 as standard OSF-RFC 86.0. PAM solves the "authentication problem", mainly, how to "integrate multiple authentication mechanisms in a modular and dynamic fashion", making PAM the de facto choice for authentication on most Unix and GNU/Linux-based systems. Linux-PAM is an implementation of PAM for GNU/Linux.</p> <p>To this day, Linux-PAM configurations are poorly understood by administrators. Ad hoc, informal PAM-configuration testing techniques exist, but suffer from many shortcomings.</p> <p>We introduce an automated, formal approach to Linux-PAM configuration testing. First, given a Linux-PAM configuration, we dynamically create an "intemal-to-the-tool" representation of a Hierarchical Coloured Petri Net (HCPN), which encodes all of the possible authentication process instances associated with this configuration. During this creation, "base case" HCPN templates are used, each template created only once, i.e. during tool development, not during testing. Second, we translate the resulting HCPN into a NuSMV model Third, we use NuSMV to verify the model for "security" properties.</p> <p>A tool prototype, implemented in C, automates these three steps. State space size was reduced via manual HCPN and Transition System specification tuning. The State Space Explosion problem was overcome with the use of NuSMV-implemented model checking algorithms. Industrial Linux-PAM configurations were tested, yielding model building times in ones of seconds, and verification times in tens of seconds. Also, the tool produces HCPN representations via Graphviz.</p>