Preventing bugs, and improving code quality with Microsoft SAL (Part 1, Prologue)

_Post_invalid_ here is kind of a hack, but it works!

You’re using an invalid handle!

Microsoft’s SAL started nearly ten years ago at Microsoft as part of a major push for code quality, and (more visibly) preventing bugchecks. In its earliest versions, it appears to have been effectively restricted to the Windows core codebase, with kernel-mode-driver developers following suit. “Unleashing the Power of Static Analysis” says that here it helped developers fix more than twenty thousands bugs in Windows Vista,  and more than 6,500 bugs in Microsoft Office 12. Of these, they found one buffer overrun per twenty annotations!

A slide from "Unleashing the Power of Static Analysis", by Manuvir Das, of the Microsoft Center for Software Excellence

A slide from “Unleashing the Power of Static Analysis“, by Manuvir Das, of the Microsoft Center for Software Excellence

Kernel-mode-driver developers have access to a much larger set of annotations, as they have much greater sensitivity to complex conditions and small bugs. Chances are, that as PC user, you’ve seen at least one blue screen that has a cryptic error message like “IRQL_NOT_LESS_OR_EQUAL”,  which means roughly that a driver tried to read memory when it shouldn’t have.

 

A slide from "Driver Annotations in Depth, Part I", by Donn Terry. Design Rule Checking is a term that you may recognize from the from the world of Electronic Design Automation, where Printed Circuit Boards are required to be within certain specifications for manufacturability.

A slide from “Driver Annotations in Depth, Part I“, by Donn Terry.
Design Rule Checking is a term that you may recognize from the from the world of Electronic Design Automation, where Printed Circuit Boards are required to be within certain specifications for manufacturability.

Proper annotation can catch this in static analysis.

A slide from Driver Annotations in Depth, Part 2, by Donn Terry

A slide from “Driver Annotations in Depth, Part 2“, by Donn Terry

See: Driver Annotations in Depth, Part 1, and Driver Annotations in Depth, Part 2

 

In “Engineering Better Software at Microsoft“, Jason Yang gives examples of ‘common-sense’ properties and behaviors, as implemented in “SAL-speak”:

SAL_Basic_properties

 

In another slide, he shows some concurrency annotations, which I’ve found invaluable:

SAL_concurrency

But most importantly, SAL has matured to become part of an even larger ecosystem:

SAL_infrastructure

SAL’s modern Infrastructure

Personally I place great emphasis on static analysis, and think others place too much emphasis on testing as a means of bug prevention.  My philosophy is that if you find bugs during testing, then you’re doing something terribly wrong. “Testing” should mean “validation“, whereby we’re pretty damned sure that everything is right. Partly, this is because we can never expect to exercise all possible conditions in testing; it’s kind of silly to try, like attempting to prove Fermat’s Last Theorem, as Prof. John Conway describes it beginning at 7:30, by testing all possible numbers – it’s never going to work.

Coming up in Part 2: using SAL to detect invalid usage of already-closed handles.

Further reading:

  1. Taming Win32 Threads with Static Analysis, by Jason Yang
  2. Advanced driver code analysis techniques

~ by Alexander Riccio on February 10, 2015.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

 
AbandonedNYC

Abandoned places and history from the five boroughs and beyond.

Open Mind

Science, Politics, Life, the Universe, and Everything

I learned it. I share it.

A software engineering blog by György Balássy

Untapped Cities

Rediscover your city: Urban discovery and exploration in NYC and around the world

Threatpost

The First Stop For Security News

Bit9 + Carbon Black Blog

#ArmYourEndpoints

The Electric Chronicles: Power in Flux

If someone ever tells you that you don't need more power, walk away. You don't need that kind of negativity in your life.

Ted's Energy Tips

Practical tips for making your home more comfortable, efficient and safe

love n grace

feel happy, be happy

Recognition, Evaluation, Control

News and views from Diamond Environmental Ltd.

greg tinkers

Sharing the successes and disasters.

Sam Thursfield's Blog

I want music in my life not questions!

Always In Motion | SAE International

A Safe, Green, Connected Blog from SAE International

Cranraspberry Blog

Sharing the things I love

Biosingularity

Advances in biological systems.

The Embedded Code

Designing From Scratch

Sean Heelan's Blog

Program analysis, verification and security

EduResearcher

Connecting Research, Practice, and Advocacy in Education

Popehat

A Group Complaint about Law, Liberty, and Leisure

Warner Stellian Appliance

Home & Kitchen Appliance Blog

Bad Science Debunked

Debunking dangerous junk science found on the Internet. Non-scientist friendly!

4 gravitons

The trials and tribulations of four gravitons and a postdoc

Strange Quark In London

A blog about physics, citylive and much procastination

The Lumber Room

"Consign them to dust and damp by way of preserving them"

In the Dark

A blog about the Universe, and all that surrounds it

andrea elizabeth

passionate - vibrant - ambitious

Probably Dance

I can program and like games

a totally unnecessary blog

paolo severini's waste of bandwidth

Musing Mortoray

Programming and Life

PJ Naughter's space

Musings on Native mode development on Windows using C++

  Bartosz Milewski's Programming Cafe

Concurrency, C++, Haskell, Category Theory

Brandon's Thoughts

Thoughts on programming

David Crocker's Verification Blog

Formal verification of C/C++ code for critical systems

Fusion

Championing a young, diverse, and inclusive America with a unique mix of smart and irreverent original reporting, lifestyle, and comedic content.

10 Minute Astronomy

Stargazing for people who think they don't have time for stargazing.

One Dev Job

notes of an interactive developer

Enterprise Architect, IoT, Cloud, Mobile Apps, Technology Evangelist, Technical Pre-Sales, Business Evangelist, Speaker

Coder/Architect for IoT, Cloud Technologies and Mobile Apps, Azure Cloud, Amazon Cloud, Windows Phone 10 Apps, iPhone Apps, Scrum Master, Business Evangelist, Mobile apps developer in iOS and Windows 10 UWP, Azure IoT Hub, Machine Learning, Stream Analytics, Azure Mobile Service, APM Tools

C++/WinRT

Modern C++ for the Windows Runtime

The Angry Technician

No, the Internet is not broken.

Kenny Kerr

Author • Systems programmer • Creator of C++/WinRT • Engineer on the Windows team • Romans 1:16

IT affinity!

The Ultimate Question of Life, the Universe, and Everything is answered somwhere else. This is just about IT.

Eat/Play/Hate

The ramblings of a crazed mind

Molecular Musings

Development blog of the Molecule Engine

%d bloggers like this: