Half-time seminar: 'Improving model learning for securing network protocol implementations'

Reviewer: Justin Pearson
Supervisors: Mohamed Faouzi Atig, Paul Fiterau, Bengt Jonsson

Abstract: Many software or hardware systems, such as security protocol implementations, must carefully manage the type and order of inputs and corresponding outputs, by maintaining a state machines which keeps track of the current state of the system. Corresponding implementation flaws, called state machine bugs, in critical systems such as security protocols can constitute serious vulnerabilities. An approach which has proven useful in uncovering state machine bugs is active automata learning, in which a model of the system is inferred through the use of test sequences. The model can then be analyzed to uncover bugs, e.g., by comparing it against the specification. In this talk, we describe two advances in the area of testing using active automata learning. The first advancement introduces an automated black-box technique for detecting state machine bugs in stateful systems. This technique uses inferred state machine models of the systems under test, in conjunction with a catalogue of known state machine bugs specified as finite automata, to find sets of sequences that (according to the inferred model) can be performed by the system and (according to the bug automaton) expose the bug.

The second advancement introduces a new learning algorithm which infers a richer class of model that can also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. Our new algorithm, SLλ, significantly reduces the number of tests required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. This results in superior performance and substantial asymptotic improvements when inferring models of bigger systems, compared to the current state-of-the-art.