Author: Julien Vanegue
In his talk at Hackito Ergo Sum conference 2010, Julien Vanegue presents a semi-automated theorem proving based approach to source code security review using the HAVOC extended static checker , a heap-aware verifier for C programs developed at Microsoft Research. His simple experiment on a single critical property fixed about fifteen memory corruption bugs in various Windows software components. Zero allocations are not bugs per se but those are signs that something odd is going on as they are rarely intended. This analysis technique is relevant on all OS including many UNIX flavors as most user-land and kernel-land allocators are exposed. His presentation also includes an original perspective on near-zero allocation vulnerabilities, in particular when the effective heap allocation size and the size-holding variable are desynchronized.