|
Pervasive
and critical software systems have dormant vulnerabilities that
attackers can trigger and cascade to make the program act as a weird
machine. In fact, they harbor exploitable programming models that can
be used to compose vulnerabilities and mount attacks. This paper
presents a type system to derive the abstract weird machines that
programs expose. The type system tracks information flow types to
detect vulnerabilities, and abstracts the control flow between
vulnerabilities to capture weird machines. We formally prove that the
inferred weird machine covers the weird runtime behaviors that the
program can exhibit. The resulting machine can then be examined to
detect patterns of attacks. An important observation is that attacks
are often simple and recurring patterns. We model the abstract machines
as regular expressions on vulnerability types. This abstract
representation is platform-independent and can be used as a uniform
description language for attacks. Further, language inclusion and
similar decisions about regular expressions are remarkably more
efficient than the same decisions for concrete programs or other formal
languages.
|
|