Summary: | The Internet, as it stands today, is highly vulnerable to attacks. However,
little has been done to understand and verify the formal security guarantees of
proposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). In
this paper, we develop a sound program logic for SANDLog-a declarative
specification language for secure routing protocols for verifying properties of
these protocols. We prove invariant properties of SANDLog programs that run in
an adversarial environment. As a step towards automated verification, we
implement a verification condition generator (VCGen) to automatically extract
proof obligations. VCGen is integrated into a compiler for SANDLog that can
generate executable protocol implementations; and thus, both verification and
empirical evaluation of secure routing protocols can be carried out in this
unified framework. To validate our framework, we encoded several proposed
secure routing mechanisms in SANDLog, verified variants of path authenticity
properties by manually discharging the generated verification conditions in
Coq, and generated executable code based on SANDLog specification and ran the
code in simulation.
|