das cav floc 06

Formal Specifications on Industrial Strength Code: From Myth to Reality: 

Formal Specifications on Industrial Strength Code: From Myth to Reality Manuvir Das Principal Researcher Center for Software Excellence Microsoft Corporation

Talking the talk …: 

Talking the talk … SAL source code annotations Deployed on Windows Vista and Office 12 Incremental approach is the key to success OPAL defect specifications Lower cost, lower coverage option Range of applicability is the key to success The right approach for the right problem SAL: focus on a small set of critical properties OPAL: apply to a wide range of quality priorities

… walking the walk: 

… walking the walk CSE impact on Windows Vista Found 100,000+ fixed bugs Added 500,000+ specifications Answered thousands of emails We are program analysis researchers But we measure our success in adoption And we feel the pain of the customer

Buffer overruns: 

Buffer overruns Defect: a buffer access index is out of bounds Detection: check that index is within bounds Problem: where are the buffer bounds stored? Tools must track buffer size from allocation to access Exhaustive global analysis is infeasible Solution: turn global analysis into local analysis Specify buffer sizes at function interfaces Perform modular (one function at a time) analysis

BO example: 

BO example Prototype of function SetupGetStringFieldW Body of function CheckInfInstead BOOL WINAPI SetupGetStringFieldW( IN PINFCONTEXT Context, IN DWORD FieldIndex, OUT PWSTR ReturnBuffer, IN DWORD ReturnBufferSize, … ); … WCHAR szPersonalFlag[20]; … SetupGetStringFieldW(andamp;Context,1,szPersonalFlag,50,…); …  

BO example: 

BO example BOOL WINAPI SetupGetStringFieldW( … __out_ecount(ReturnBufferSize) OUT PWSTR ReturnBuffer, IN DWORD ReturnBufferSize, …); WCHAR szPersonalFlag[20]; … SetupGetStringFieldW(andamp;Context,1,szPersonalFlag,50,NULL); NT# 587620 PREfast: \nt\inetsrv\iis\setup\osrc\dllmain.cpp dllmain.cpp(112) : warning 202: Buffer overrun for stack buffer 'szPersonalFlag' in call to 'SetupGetStringFieldW': length 100 exceeds buffer size 40.

SAL example 1: 

SAL example 1 wcsncpy [precondition] destination buffer must have enough allocated space wchar_t wcsncpy ( wchar_t *dest, wchar_t *src, size_t num ); wchar_t wcsncpy ( __pre __notnull __pre __writableTo(elementCount(num)) wchar_t *dest, wchar_t *src, size_t num ); wchar_t wcsncpy ( __out_ecount(num) wchar_t *dest, wchar_t *src, size_t num);

SAL example 2: 

SAL example 2 memcpy void * memcpy ( void * dest, void * src, size_t num ); void * memcpy ( __pre __notnull __pre __writableTo(byteCount(num)) __post __readableTo(byteCount(num)) void * dest, __pre __notnull __pre __deref __readonly __pre __readableTo(byteCount(num)) void * src, size_t num ); void * memcpy ( __out_bcount_full(num) void * dest, __in_bcount(num) void * src, size_t num );

Standard Annotation Language: 

Standard Annotation Language Usage example: a0 RT func(a1 … an T par) ai : SAL annotation Interface contracts pre, post, object invariants Basic properties null, readonly, valid, range, … Buffer extents writableTo(size), readableTo(size) Buffer size formats (byte|element)Count, endPointer, sentinel, …

SAL ecosystem: 

SAL ecosystem espX/PREfast/… : Use annotations to find defects SALstats : Identify parameters that should be annotated MIDL Compiler : Translate MIDL directives to annotations SALinfer : Infer annotations using global static analysis

SALinfer example: 

SALinfer example size(tmp,200) size(buf,len) size(buf2,len) size(buf2,len2) size(buf,len) write(buf) write(buf) write(buf) write(buf2) void work() { int tmp[200]; wrap(tmp, 200); } void wrap(int *buf, int len) { int *buf2 = buf; int len2 = len; zero(buf2, len2); } void zero(int *buf, int len) { int i; for(i = 0; i andlt;= len; i++) buf[i] = 0; }

SALinfer example: 

SALinfer example void work() { int tmp[200]; wrap(tmp, 200); } void wrap(__out_ecount(len) int *buf, int len) { int *buf2 = buf; int len2 = len; zero(buf2, len2); } void zero(__out_ecount(len) int *buf, int len) { int i; for(i = 0; i andlt;= len; i++) buf[i] = 0; }

espX example: 

espX example void zero(__out_ecount(len) int *buf, int len) { int i; for(i = 0; i andlt;= len; i++) buf[i] = 0; } Subgoal 2: i andlt; sizeOf(buf) assume(sizeOf(buf) == len) inv (i andgt;= 0 andamp;andamp; i andlt;= len) Constraints: (C1) i andgt;= 0 (C2) i andlt;= len (C3) sizeOf(buf) == len Goal: i andgt;= 0 andamp;andamp; i andlt; sizeOf(buf) Subgoal 1: i andgt;=0 by (C1) Warning: Cannot validate buffer access. Overflow occurs when i == len Subgoal 2: i andlt; len by (C3) Subgoal 2: i andlt; len FAIL assert(i andgt;= 0 andamp;andamp; i andlt; sizeOf(buf))

SAL impact: 

SAL impact Windows Vista Mandate: Annotate 100,000 mutable buffers Developers annotated 500,000+ parameters Developers fixed 20,000+ bugs Office 12 Developers fixed 6,500+ bugs Visual Studio, SQL, Exchange, … External customers CRT + Windows headers SAL annotated SAL aware compiler shipped with VS 2005

SAL evaluation: 

SAL evaluation Vista – mutable string buffer parameters Annotation cost: [–] 100,000 parameters required annotations [+] 4 out of 10 automatic Defect detection value: [+] 1 buffer overrun exposed per 20 annotations Locked in progress: [+] 9.4 out of 10 buffer accesses validated

SAL priorities: 

SAL priorities Crashes Annotate possibly-NULL pointers (SALinfer) Enforce NULL pointer checking (PREfast) Error handling Annotate failure conditions (SALinfer, typedefs) Enforce error handling in callers (PREfast) AppCompat Annotate public APIs (MaX, WINAPI macros) Prohibit signature changes (SD) Resource usage, drivers, …

Annotations summary: 

Annotations summary Ensure correct behavior by extending the type system with SAL annotations [+] Checkers validate correct behavior [–] Requires investment in annotation effort [–] Requires investment in developer education SAL is a high cost, high return approach Applicable to a small class of critical defects

OPAL – defect by example: 

OPAL – defect by example Problem A defect is discovered through internal testing, or in the field (MSRC, Watson) Diagnosis Identify the code pattern that caused the bug Detection Specify the code pattern formally in OPAL Use checkers to find instances of the pattern

RegKey leak defect: 

RegKey leak defect status = RegOpenKeyExW( HKEY_LOCAL_MACHINE,    L'SOFTWARE\\Microsoft\\Windows NT\\CurrentVersion\\Perflib',    0L, KEY_READ, andamp; hLocalKey); if (status == ERROR_SUCCESS) bLocalKey = TRUE; … block of code that uses hLocalKey … if (bLocalKey) CloseHandle(hLocalKey); Bug: registry key is closed by calling the generic CloseHandle API May fail to clean up some data that is specific to registry key data structures

RegKey leak code pattern: 

RegKey leak code pattern Search for code paths along which a registry key is opened, and then closed using the generic CloseHandle API Specification: define a sequence of relevant actions e.g. A(k)…B(h) define the actions (e.g. A, B, k and h)

RegKey leak specification: 

RegKey leak specification defect RegKeyCloseHandle { // A(x)…B(x) sequence OpenKey(key);CloseHandle(handle) message 'Registry key closed using generic CloseHandle API!' // A(x) pattern OpenKey(key) /RegOpenKeyEx[AW](@\d+)?$/ (_,_,_,_,andamp;key) where (return == 0) // B(x) pattern CloseHandle(handle) /CloseHandle(@\d+)?$/ (handle) } This is the entire specification effort for the codebase

OPAL – under the hood: 

OPAL – under the hood Requirements for checkers Customizable analysis engine Path-specific static or dynamic analysis Checking support for OPAL Vista: ESP (global static analysis) Vista: PREfast (local static analysis) truScan (execution trace analysis)

Safety properties: 

Safety properties void main () { if (dump) fil = fopen(dumpFile,'w'); if (p) x = 0; else x = 1; if (dump) fclose(fil); } void main () { if (dump) Open; if (p) x = 0; else x = 1; if (dump) Close; }

ESP: 

ESP Symbolic state: FSA + execution state Branch points: Does execution state uniquely determine branch direction? Yes: process appropriate branch No: split andamp; update state, and process both branches Merge points: Do states agree on FSA? Yes: merge states No: process states separately

ESP example: 

ESP example [Opened|dump=T] [Closed] [Closed|dump=T] [Closed|dump=F] [Opened|dump=T] [Closed|dump=F] [Closed]

OPAL impact: 

OPAL impact

OPAL priorities: 

OPAL priorities Concurrency Specify incorrect lock usage Localization Specify usage of culture-sensitive strings Accessibility Specify usage of hard-coded fonts and colors DLL loading Specify cyclic dependencies from DLLMain Security, drivers, serviceability, …

Specifications summary: 

Specifications summary Rule out specific patterns of incorrect behavior by writing OPAL specifications of observed failures [+] Specifications are written once per codebase [+] Education is limited to a few experts [–] No validation ('how far are we from done?') OPAL is a low cost, lower return approach Applicable to a broad range of quality priorities

Formal specifications roadmap: 

Formal specifications roadmap Critical properties Buffer overruns Integer overflows NULL dereferences … Quality priorities Attack surface reduction Concurrency Localization … IDEAL IDEAL Code Review PREfix/ PREfast PREfast OPAL Testing SAL

Lessons : 

Lessons

Forcing functions for change: 

Forcing functions for change Gen 1: Manual Review Too many code paths to think about Gen 2: Massive Testing Inefficient detection of simple errors Gen 3: Global Program Analysis Delayed results Gen 4: Local Program Analysis Lack of calling context limits accuracy Gen 5: Specifications

Developers like specifications: 

Developers like specifications If you make them incremental No specifications, no bugs If you make them useful More specifications, more real bugs If you make them informative Make implicit information explicit Avoid repeating what the code says

Defect detection myths: 

Defect detection myths Soundness matters sound == find only real bugs The real measure is Fix Rate Completeness matters complete == find all the bugs There will never be a complete analysis Developers only fix real bugs Developers fix bugs that are easy to fix, and Unlikely to introduce a regression

Theory is important: 

Theory is important Fundamental ideas have been crucial Hoare logic Dataflow analysis Abstract interpretation Graph algorithms Context-sensitive analysis Alias analysis

Summary: 

Summary Goal: Use formal specifications to move enforcement of code quality upstream Testing  Specifications  Compiler Two complementary solutions: Source code annotations (SAL), targeted to a small set of critical properties Defect specifications (OPAL), applied to a wide range of quality priorities Testing  OPAL  SAL  Compiler

Slide36: 

© 2006 Microsoft Corporation. All rights reserved. This presentation is for informational purposes only. MICROSOFT MAKES NO WARRANTIES, EXPRESS OR IMPLIED, IN THIS SUMMARY. http://www.microsoft.com/cse http://research.microsoft.com/manuvir