home Anil Madhavapeddy, Professor of Planetary Computing  

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

Anil Madhavapeddy.

Paper in the formal Methods and Software Engineering.

URL (link.springer.com)   DOI   BIB   PDFpdf

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 model-checked 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.

# 1st Nov 2009   iconpapers conference dsl formal fp security

Related News