A Structured Approach to Network Security Protocol Implementation

Tobler, Benjamin (2005) A Structured Approach to Network Security Protocol Implementation, MSc.

PDF ben-tobler-2005-12-thesis.pdf Download (1MB)

Abstract

The implementation of network security protocols has not received the same level of attention in the literature as their analysis. Security protocol analysis has successfully used inference logics, like GNY and BAN, and attack analysis, employing state space examination techniques such as model checking and strand spaces, to verify security protocols. Tools, such as the multi-dimensional analysis environment SPEAR II, exist to help automate security protocol specification and verification, however actual implementation of the specification in executable code is a task still largely left to human programmers. Many vulnerabilities have been found in implementations of security protocols such as SSL, PPTP and RADIUS that are incorporated into widely used operating system software, web servers and other network aware applications. While some of these vulnerabilities may be a result of flawed or unclear specifications, many are the result of the failure of programmers to correctly interpret and implement them. The above indicates a gap between security protocol specifications and their concrete implementations, in that there are methodologies and tools that have been established for developing the former, but not the latter. This dissertation proposes an approach to bridging this gap, describes our implementation of that approach and attempts to evaluate its success. The approach is three-fold, providing different measures to improve current ad-hoc implementation approaches: 1. From Informal to Formal Specifications: If a security protocol has been specified using informal standard notation, it can be converted, using automatic translation, to a formal specification language with well defined semantics. The formal protocol specification can then be analysed using formal techniques, to verify that the desired security properties hold. The precise specification of the protocol behaviour further serves to facilitate the concrete implementation of the protocol in code. 2. Separate Implementation Concerns: When implementing security protocols, the what and the when of protocol actions are abstracted from the how. That is, protocol logic implementation concerns, such as when and what actions should be performed on messages, should be clearly and cleanly separated from the cryptographic and network communication implementation details that implement how the actions are performed. Such high level modularity allows code implementing protocol logic to be re-used with different cryptographic algorithm implementations and network communication protocols. It also allows errors in the implementation of the cryptography to be addressed by swapping cryptographic implementations without changing the protocol logic code. The abstraction of cryptographic and network implementation is analogous to the adoption of the Dolev-Yao style models by many analysis techniques, where the cryptography itself is viewed as a black box and assumed perfect, allowing the analysis to focus on the protocol logic. Finally, this separation allows the correctness of the protocol logic implementation and cryptographic primitives implementation to be addressed separately. 3. Automated Implementation Using Code Generation We use code generation to automate the security protocol implementation process, avoiding the risk of human error in interpreting the sometimes subtle semantics of security protocol specifications. The precise nature of formal specification languages provides a base from which to specify and implement an automatic code generation tool. Our approach follows requirements identified for high integrity code generation - where feasible - to give a high level of confidence in the correctness of the generated code. In implementing the approach, we adopt the Spi Calculus for the role of formal specification language. The Spi Calculus was developed by extending the -calculus, a process algebra for describing concurrent communicating systems, to cater for the special case of network security protocols. Spi Calculus specifications can be analysed manually, by developing correctness proofs by hand, and automatically, by using model checkers such as MMC. As Spi Calculus specifications explicitly describe the actions of a security protocol, they are also particularly suitable for use as input for code generation. The implementation of the approach is split across three components that correspond to each of the parts of the approach: 1. Sn2Spi is a translator that converts an informal standard notation specification to a Spi Calculus specification, thus implementing part 1 of our approach. The converted specification can be analysed using any of the formal techniques applicable to the Spi Calculus. Once verified, the specification can be used to generate a concrete implementation using Spi2Java. 2. The Security Protocol Primitives API abstracts cryptographic and network communication operations, decoupling code that implements protocol logic from code that implements cryptographic and network operations. It provides the basic cryptographic and network communications functionality required to implement a security protocol, including: symmetric and asymmetric encryption, message digest, nonce and timestamp generation, marshalling message component data and sending and receiving messages over a network. A provider model, much like that used in the Java Cryptography Extensions API, is employed to allow different implementations to be swapped without changing the SPP client code. 3. Spi2Java is a code generator, essentially implementing a compiler from the Spi Calculus to Java code. Spi2Java uses Prolog to implement a defined mapping from Spi Calculus constructs, i.e. terms and process actions, to Java code segments. These code segments call the SPP API to access cryptographic and network functionality where needed. The mapping was developed by refining Spi constructs to Java code segments that preserve the semantics of the Spi constructs In addition, assertions are made in the code segments to ensure certain conditions are met before the implementation can continue running. Part of evaluating the effectiveness of this automated approach to security protocol implementation, involved a case study where manual implementations of the CCITT Three Message X.509 Protocol, developed by 4th year Computer Science students, and a Spi2Java generated implementation are compared. The outcome of the study favoured the automatically generated implementation, indicating the potential of the approach. Further to demonstrating the utility of code generation, we describe an SPP provider implementation developed to allow a security protocol run, including legitimate and attacker roles, to be simulated in a controlled environment. Spi2Java allows the protocol engineer to quickly and automatically generate code for protocol roles. The code can be executed using this implementation allowing the protocol engineer to step through execution of all roles, both legitimate and attacker, to gain insight into the behaviour of the protocol. The approach is evaluated in terms of the class of attacks it prevents and how it meets the identified requirements for high integrity code generation. It is also compared to existing and current work in the field. Attack classes that exploit faulty protocol logic implementation, vulnerability to type flaws and buffer overflows are prevented. The Spi2Java code generator fully meets three of the five high integrity code generation requirements: formally defined source and target languages are used; the translation software is validated; and the generated code is well structured and documented and can be traced back to the specification. Spi2Java partially meets the requirement that the mapping from source to target language constructs be formally proven to preserve the specification semantics. However the arguments given are not strictly formal. The requirement related to rigorous testing are not met due to practical resource constraints. However, Spi2Java has been used to generate real world protocol implementations that have been verified by manual inspection. Sprite, incorporating the Sn2Spi translator and Spi2Java code generator, provides a structured approach to network security protocol implementation by implementing automated translation from informal to formal security protocol specifications, and by being able to automatically generate Java implementations of network security protocols in which the security protocol engineer can have a high degree of confidence.

Item Type:	Electronic thesis or dissertation (MSc)
Date Deposited:	20 Dec 2005
Last Modified:	10 Oct 2019 15:35
URI:	http://pubs.cs.uct.ac.za/id/eprint/281

Actions (login required)

View Item