Specification Inference for Security

robk — Fri, 27 Feb 2009 01:04:00 GMT

Aditya Nori, a researcher in the Rigorous Software Engineering team at Microsoft Research India, just gave me a brief overview of his demo, entitled Specification Inference for Security, and as he made repeated references to the poster in his TechFest booth, I though it would be instructive to share:

A higher-resolution version is available that enables you to enlarge the poster to read through everything, but the key to the project--a new algorithm that automatically infers explicit information-flow security specifications from program code--is located under Specification on the left-hand side of the poster, which defines the classification of nodes in a data-flow graph of program code as "sources," "sinks," or "sanitizers." A source is a node that returns tainted, bad data. A sink receives that bad data, and a sanitizer cleans the data, so that even if it receives tainted data, it does not pass it along. It's a case of garbage in/no garbage out.

"This project is about improving the quality of existing static-analysis tools for security," Nori explains. "Most automated tools for security rely on specifications, because they really need to know what they're searching for. Our job here is to go through the programs and automatically infer specifications in the program."

He points to the "Information flow vulnerabilities" portion of the poster and to the node named ReadData1.

"If you look at this code fragment," Nori continues, "here's a data-flow graph of the response to this code fragment. Information flows from this method or function call into this function call [Prop1]. If I just went though this graph and asked if there was something wrong, if there's a bug over here, it's hard to say, because you need more context.

"That's exactly what a static-analysis tool is going to say: You need to provide more information, and you need to say what the problem is. On the other hand, if I consider this a source, a producer of taint, and that one a sink, a consumer of taint, then the static-analysis tool will be able to say that the first part is a bad part. There could be a malicious user sending some data that screws up your database. If this [Cleanse] was a cleanser, which actually checks that whatever is being passed on to the database is safe data, then this part is OK. What the static-analysis tool needs to know, in addition to your program, is the role of every function in your program: Here's a function of source, here's a function of sink, here's a function of sanitizer."

In the real world of software development, though, that's an improbable scenario.

"It's really unreasonable to assume that if somebody is presented with 1 million lines of code, they're actually, mindfully going to go through the code and annotate every method as a source, sink, or sanitizer," Nori stipulates. "That's unacceptable. No developer is going to do it. So what we do is go through the code and automatically analyze the code and annotate every function as a source, sink, or sanitizer."

He turns to the Architecture section of the poster.

"Here's a high-level overview," he says. "We take the program, do static analysis, and convert it into a data-flow graph. The data-flow graph includes a bunch of constraints. For technical reasons, it's helpful to look upon these constraints as probabilistic constraints We take the data-flow graph, convert it into this probabilistic model, and feed that to a constraint solver. The solution to the set of constraints precisely tells us which methods in our program correspond to sources, sinks, and sanitizers."

And in a real-life test, the technique worked wonders.

"We ran our tool on 10 critical Microsoft business applications," Nori reports, "and we discovered 67 new sources, 25 new sanitizers, and 75 new sinks. The next step for us was to assess the quality of these specifications. Did these specifications really improve the quality of an existing static-analysis tool? We took a static-analysis tool that is being developer by Microsoft for security and ran that tool on these applications. The tool discovered 89 vulnerabilities, of which 20 were false positives. Then we ran the tool again with our new specifications, and we discovered 335 vulnerabilities. We were very excited about that. Another nice thing about our specifications is that they eliminated 13 of the 20 false positives from this set."

Such numbers grab attention within Microsoft, and there is a strong possibility that the specification-inference algorithm might be included in an upcoming product release. Successful technology transfer makes researchers smile, but Nori knows there is much left to be done.

"My collaborators believe this is a new way of analyzing programs, combining program analysis with statistical analysis," he says. "We are a long ways from applying this to other domains and program analysis. That's the future of this project. We look at this project as the starting point for combining program analysis and statistical analysis."

TechFest Live! : Aditya Nori

Specification Inference for Security