Trusted Key Manager for IKEv2
HSR University of Applied Sciences Rapperswil Switzerland
IPsec relies on the correct operation of the Internet Key Exchange (IKE) protocol to meet its security goals. The implementation of IKE is a non-trivial task and results in a large and complex code base. This makes it hard to gain a high degree of confidence in the correct operation of the code.
Reto Buerki and Adrian-Ken Rueegsegger from the University of Applied Sciences in Rapperswil have proposed a component-based approach by disaggregating IKEv2 into trusted and untrusted components to attain a higher level of security. By formulating security properties and identifying the critical components of the IKEv2 protocol, a concept to split the key management system has been presented.
The security-critical part represents a trusted computing base (TCB) and is termed Trusted Key Manager (TKM). Care was taken to only extract the functionality that is absolutely necessary to ensure the desired security properties. Thus, the presented interface between the untrusted IKEv2 processing component and TKM allows for a small and robust implementation of the TCB. The splitting of the protocol guarantees that even if the untrusted side is completely subverted by an attacker, the trusted components uphold the proposed security goals.
The TKM has been implemented from scratch using the Ada programming language. The new Design-by-Contract feature of Ada 2012 has been used for the implementation of state machines, to augment the confidence of operation according to the specification. The TKM works in conjunction with the strongSwan IKEv2 daemon to provide key management services for IPsec.
Read the project report http://www.codelabs.ch/tkm/ike-separation.pdf
Visit the TKM project page http://www.codelabs.ch/tkm/
Visit the strongSwan project page http://www.strongswan.org/