Driller paper said this is about angr.

1 Firmalice uses SE engine and some techniques such as program slicing. They are looking for bypass flaws in firmware. 2 Firmware often runs directly on hardware without OS. It is just a binary blob. Modification is hard because of cryptographical signing. Firmalice recieves blob and specification of its security policy, translates binary code into an IR, and performs a static full-program control and data flow analysis, followed by SE of slices. It based on input determinism concept.

3 Devices contain privileged operations accessible only by authorized users. Types of authentication bypass: (1) hardcoded authentication credentials, (2) hidden (undocumented) authentication interface (without auth.), (3) bugs (e.g. command injections). Goal is to generate input that leads to path from entry point to privileged operation. Can we use our directed analysis? Authentication bypass is a logic vulnerability instead of, for example, memory corruption vulnerability (buffer overflow). And it is required privileged operation specification.

4 Firmalice performs static analysis for CFG and DDG extraction and authentication slice from entry to priveleged point creation. And then SE to reach privileged point. Authentication slice is a set of nodes which may contains needed path (all possible paths).

7 Their symbolic execution engine is based on ideas of KLEE, FuzzBALL, and Mayhem. It is performed on authentication slice. 8 And it has support for symbolic summaries of functions (detect common library functions and abstract their effects on the symbolic state). They use 49 manually written abstractions. They use sets of test cases to determine if some arbitrary binary function is an implementation of the summarized function.

Sergey Vartanov, 2007–2020