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.