[PRL] [Fwd: Be Blackburn] How to Get Annotations & Specificationsinto Industrial Code: Three easy lessons

Paul Steckler steck at stecksoft.com
Fri Jun 20 17:31:30 EDT 2003


I attended, but did not take notes.  Here's an executive 
summary.

The Office group adds a few annotations to C code, which 
are read by Weise's PreFAST toolkit, which exposes Visual C++
parse trees.  Static analyzers written with the toolkit do 
very simple things, like interval analysis to detect out-of-range 
buffer indices.  They had to rejigger the internal Office APIs so 
that all procedures that take a buffer argument also receive read and 
write "extents", or sizes.  Apparently, lots of bugs were found this
way.

A lot of the annotations are generated from Hungarian notation
types, maybe 20% have been added by hand.  

All this happened after Code Red and Nimba convinced MS 
management that security might be a real issue.

Although he didn't describe them in detail, the static analysis 
techniques were completely unsophisticated, probably dating from the 
1960's.  

-- Paul

> -----Original Message-----
> From: prl-bounces at lists.ccs.neu.edu 
> [mailto:prl-bounces at lists.ccs.neu.edu] On Behalf Of Mitchell Wand
> Sent: Tuesday, June 10, 2003 7:38 PM
> To: PRL mailing list
> Subject: [PRL] [Fwd: Be Blackburn] How to Get Annotations & 
> Specificationsinto Industrial Code: Three easy lessons
> 
> 
> anybody gonna go and take notes?
> 
> --Mitch 
> 
> ------- start of forwarded message (RFC 934 encapsulation) -------
> Return-Path: <be at egret.lcs.mit.edu>
> Delivered-To: wand at ccs.neu.edu
> From: Be Blackburn <be at theory.lcs.mit.edu>
> To: toc at egret.lcs.mit.edu
> Subject: How to Get Annotations & Specifications into 
> Industrial Code: Three easy lessons
> Date: Mon, 9 Jun 2003 12:01:19 -0400
> 
> TALK Friday, June 20th
> Talk: How to Get Annotations and Specifications into 
>       Industrial Code: Three easy lessons
> Speaker: Daniel Weise, Senior Researcher, Microsoft Office
> Host: Michael Ernst, LCS
> 
> Date:	06-20-2003
> Time:   1:30 PM - 2:30 PM
> Food:	1:15 PM
> Where:  Room NE43-518
> 
> In response to necessity for more reliable products, 
> Microsoft development groups are rapidly moving towards code 
> annotations and domain specific checkers for those 
> annotations. Yet common wisdom from the academic community 
> had it that you could never get developers to annotate their 
> code. How did this happen? 
> 
> This talk will cover the current state of code annotation and 
> checking technology at Microsoft, how we got developers to 
> annotate code, and where we are headed. As a specific 
> example, I will also cover my buffer overrun detector, which 
> works surprisingly well because Office has bought into a 
> dependent type system (based on code annotation) in an 
> attempt to turn buffer overruns into type errors.
> 
> Bio:
> 
> Daniel Weise has advanced degrees from a respectable place 
> (M.I.T.), been faculty at a nearly respectable place 
> (Stanford University), and run a successful research group at 
> a industrial place (Microsoft
> Research) where his research group designed and built program 
> analysis technology that is having tremendous impact on the 
> quality of Microsoft products. In spite of his background, or 
> maybe because of it, he now insists on slumming in product 
> groups because that's where he believes the important action 
> is, and that it's how to best effect change and how to get 
> the good ideas from research put into practice and have 
> research ideas informed by practice.  He has been championing 
> code annotation for three years from within the Office 
> product group, and this effort has paid off big time.
> 
> Relevant URL(S): 
> 
> For more information please contact: 
> Neena Lyall, 617-253-6019
> lyall at lcs.mit.edu 
> ------- end ------- _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu https://lists.ccs.neu.edu/bin/listinfo/prl
> 



More information about the PRL mailing list