[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