LCA: The Trinity fuzz tester

Posted Feb 7, 2013 1:43 UTC (Thu) by michaelr (subscriber, #73025) [Link]

Annotating source code to do static analysis is not new to practical user-space programs. Microsoft has long used and advocated its Static Annotation Language (http://msdn.microsoft.com/en-us/library/ms182032.aspx), which captures many of the same concepts as Trinity's annotation system.

SAL annotates the function prototypes directly; the nearest equivalent to the madvise() Trinity annotation above would be something like:

int madvise(
  _In_reads_bytes_(length) void *addr,
  _In_ size_t length,
  _In_ _In_range_(MADV_NORMAL, MADV_UNMERGEABLE) int advice
);

The _In_reads_bytes_(length) tag on addr captures the Trinity annotations for both addr and length. I've assumed that MADV_NORMAL is the numerically lowest advice value and MADV_UNMERGEABLE is the highest, as SAL doesn't deal well with enumeration constants that aren't defined in an enum type.

Microsoft requires use of SAL in all its C and C++ code as part of its Security Development Lifecycle (http://msdn.microsoft.com/en-us/library/windows/desktop/cc307398.aspx), and advocates its uses by third-party application and driver developers on Windows. I don't know whether they use it for fuzzing guidance as Trinity does, but I do know that they have at least two static analyzers that understand it (one of which ships with recent versions of their compiler) and they feel it to have helped tremendously in writing more secure code.