Full paper: Postscript, PS.GZ, PDF

The Code Generator

Our goal for the automatic code generator is to prevent implementation weaknesses, and obtain a secure implementation if the initial protocol is secure. The code generator is essentially a translator which translates the formal specification into Java code. Given that the translation rules are correct, the final implemenation can be shown to be correct using proof by construction. In particular, we show that our implementation is secure against some of the most common vulnerabilities:

• Buffer overruns account for more than half of all recent security vulnerabilities. Since we use Java as our implementation language, our automatically generated code is immune against this class of attack.
• False input attacks result from unchecked input parameters or unchecked conditions or errors. Our automatic implementation ensures that all input parameters are carefully checked to have the right format before used.
• Type flaws occur when one message component can be interpreted as another message component of a different form. In the implementation, we use typed messages to prevent type flaws.
• Replay attacks and freshness attacks are attacks where the attacker can reuse old message components in the attack. Athena already ensures that the protocols are secure against these attacks. To ensure that the implementation is secure, we use cryptographically secure pseudo-random number generators to create secure nonces.

The code generator uses the same protocol description as Athena uses. The generated code provides a simple yet flexible API for the application programmer to interface with. More details about the code generator can be found in [PPS00].

 


Figure 1: AGVIGUI