Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language

Internet protocols encapsulate a significant amount of state, making implementing the host software complex. In this paper, we define the Statecall Policy Language (SPL) which provides a usable middle ground between ad-hoc coding and formal reasoning. It enables programmers to embed automata in their code which can be statically modelchecked using SPIN and dynamically enforced. The performance overheads are minimal, and the automata also provide higher-level debugging capabilities. We also describe some practical uses of SPL by describing the automata used in an SSH server written entirely in OCaml/SPL. Constructing modern Internet servers is a difficult proposition, since the software must encapsulate a significant amount of state and deal with a variety of incoming packet types, complex configurations and versioning inconsistencies. Network applications are also expected to be liberal in interpreting received data packets and must reliably deal with timing and ordering issues ari...

• Type: Conference
• Year: 2009
• Where: ICFEM
• Authors: Anil Madhavapeddy
• Keywords: Abstract Model, ICFEM 2009, Model Checking, Software Engineering, Statecall Policy Language