Sciweavers

Share
ICFEM
2009
Springer

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

9 years 1 months ago
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...
Anil Madhavapeddy
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ICFEM
Authors Anil Madhavapeddy
Comments (0)
books