Code annotations for static analysis in user-space
Posted Feb 7, 2013 1:43 UTC (Thu) by michaelr
In reply to: LCA: The Trinity fuzz tester
Parent article: LCA: The Trinity fuzz tester
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:
_In_reads_bytes_(length) void *addr,
_In_ size_t length,
_In_ _In_range_(MADV_NORMAL, MADV_UNMERGEABLE) int advice
captures the Trinity annotations for both
. I've assumed that
is the numerically lowest advice value and
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.
to post comments)