Inspecting the source code that implements the PPP Protocol in Linux


Srdjan Rusovan



Abstract

The Point-to-Point Protocol (PPP) is a widely accepted standard used by almost everyone who connects to a server over a telephone line. An open source implementation of the PPP protocol, pppd - the PPP daemon, is included in various Linux distributions and widely used by Linux users. Version 2.4.1 of the pppd is typical of many software products in that the only documentation available is the C programming language code and a high-level requirements document containing an English language description of the system's required behaviour, together with the state transition table for the protocol's abstract state machine. In order to perform a rigorous inspection of the pppd protocol state machine code based upon Parnas' Display method, we required detailed design documents that simply did not exist. In [Parnas 1994] a rigorous inspection method which manually generates the absent design documentation and performs the inspection, is presented. This thesis shows how parts of the process can be automated using theorem proving techniques. Specifically, the reverse engineering of the design documentation was primarily done in PVS Specification and Verification System. The resulting combination of inspection based upon the Display method and theorem proving was used to find several mistakes in the PPP implementation code. Inconsistency in coding style and significant issues regarding the readability of the code were also discovered. Thus the thesis also provides a detailed example of successful application of the Displays inspection method to a non-trivial application.