Verification State-Space Reduction Through Restricted Parsing Environments

Explore a presentation on reducing verification state-space through restricted parsing environments. Learn about the LangSec principles for constructing input-handling software and their potential to significantly reduce the size and complexity of verification tasks. Discover Crema, a sub-Turing programming language and restricted execution environment, and examine a case study comparing verification task sizes for Qmail SMTP parsing code fragments in native execution versus Crema. Delve into the application of these principles to reference monitor verification, and gain insights into future work in this field. The talk covers topics such as input parsing, open source, static analysis, formal tools, and contextual implementation, providing a comprehensive overview of state-space reduction techniques in software verification.

Introduction
Goals
CLE
The Problem
The Circle of Life
Input Parsing
Open Source
Fizzbuzz
Graph
Reference Monitors
Future Work
Thanks
Questions Discussion
What an attacker can do
Static analysis and formal tools
Bridging the gap
Contextual implementation