NaCl to give way to RockSalt: Computer scientists develop a tool to improve software fault isolation

Jul 20, 2012

A team led by Harvard computer scientists, including two undergraduate students, has developed a new tool that could lead to increased security and enhanced performance for commonly used web and mobile applications.

Called RockSalt, the clever bit of code can verify that native computer programming languages comply with a particular security policy.

Presented at the ACM Conference on Programming Language Design and Implementation (PLDI) in Beijing, in June, RockSalt was created by Greg Morrisett, Allen B. Cutting Professor of Computer Science at the Harvard School of Engineering and Applied Sciences (SEAS), two of his undergraduate students Edward Gan '13 and Joseph Tassarotti '13, former postdoctoral fellow Jean-Baptiste Tristan (now at Oracle), and Gang Tan of Lehigh University.

"When a user opens an external application, such as Gmail or Angry Birds, web browsers such as Chrome typically run the program's code in an intermediate and safer language such as JavaScript," says Morrisett. "In many cases it would be preferable to run native machine code directly."

The use of native code, especially in an online environment, however, opens up the door to hackers who can exploit vulnerabilities and readily gain access to other parts of a computer or device. An initial solution to this problem was offered over a decade ago by at the University of California, Berkeley, who developed software fault isolation (SFI).

SFI forces native code to "behave" by rewriting machine code to limit itself to functions that fall within particular parameters. This "sandbox process" sets up a contained environment for running native code. A separate "checker" program can then ensure that the executable code adheres to regulations before running the program.

While considered a major breakthrough, the solution was limited to devices using RISC chips, a processor more common in research than in consumer computing. In 2006, Morrisett developed a way to implement SFI on the more popular CISC-based chips, like the Intel x86 processor. The technique was adopted widely. Google modified the routine for Google Chrome, eventually developing it into Google Native Client (or "NaCl").

When bugs and vulnerabilities were found in the checker for NaCl, Google sent out a call to arms. Morrissett once again took on the challenge, turning the problem into an opportunity for his students. The result was RockSalt, an improvement over NaCl, built using Coq, a proof development system.

"We built a simple but incredibly powerful system for proving a hypothesis—so powerful that it's likely to be overlooked. We want to prove that if the checker says 'yes,' the code will indeed respect the sandbox security policy," says Joseph Tassarotti '13, who built and tested a model of the execution of x86 instructions. "We wanted to get a guarantee that there are no bugs in the checker, so we set out to construct a rigorous, machine-checked proof that the checker is correct."

"Our proofs about the correctness of our own tool say that if you run the tool on a program, and it says it's safe to run, then according to the model, this program can only do certain things," Tassarotti adds. "Our proof, however, was only as good as this model. If the model was wrong, then the tool could potentially have an error."

In other words, he explains, think of an analogy in physics. While you might mathematically prove that according to Newton's laws, a moving object will follow a certain trajectory, the proof is only meaningful to the degree that Newton's laws accurately model the world.

"Since the x86 architecture is very complicated, it was essential to test the model by running programs on a real chip, then simulating them with the model, and seeing whether the results matched. I specified the meanings of many of these instructions and developed the testing infrastructure to check for errors in the model," Tassarotti says.

Even more impressively, RockSalt comprises a mere 80 lines of code, as compared to the 600 lines of the original Google native code checker. The new checker is also faster, and, to date, no vulnerabilities have been uncovered. The tool offers tremendous advantages to programmers and users alike, allowing programmers to code in any language, compile it to native executable code, and secure it without going through intermediate languages such as JavaScript, and even to cross back and forth between Java and native code. This allows coders to choose the benefits of multiple languages, such as using one to ensure portability while using others to enhance performance.

"The biggest benefit may be that users can have more peace of mind that a piece of software works as they want it to," says Morrisett. "For users, the impact of such a tool is slightly more tangible; it allows users to safely run, for example, games, in a web browser without the painfully slow speeds that translated code traditionally provides."

Previous efforts to develop a robust, error-free checker have resulted in some success, but RockSalt has the potential to be scaled to software widely used by the general public. The researchers expect that their tool might end up being adopted and integrated into future versions of common web browsers. Morrisett and his team also have plans to adapt the tool for use in a broader variety of processors.

Reflecting on how the class project has been transformative, Tassarotti says, "I plan to pursue a Ph.D. in computer science, and I hope to work on projects like this that can improve the correctness of software. As computers are so prevalent now in fields like avionics and medical devices, I believe that this type of research is essential to ensure safety."

Explore further: Atari's 'E.T.' game joins Smithsonian collection

Related Stories

Google Dart debut sparks chatter of JavaScript coup

Oct 12, 2011

(PhysOrg.com) -- When the news appeared earlier this week that Google was unveiling a new programming language, Dart, for developers. tech blogs ignited with talk of how Google is staging a JavaScript coup. ...

Google Go gets going (w/ Video)

Nov 11, 2009

(PhysOrg.com) -- Google has introduced its new experimental programming language Go, which aims to combine speedy application development through simplified coding with high-speed program execution.

Java Security Traps Getting Worse

May 10, 2007

A year ago at JavaOne , Fortify Software Founder and Chief Scientist Brian Chess gave a presentation titled " 12 Java Technology Security Traps and How to Avoid Them ."

New programming language to plug information leaks in software

Nov 23, 2011

The current method for preventing users and unauthorised individuals from obtaining information to which they should not have access in data programs is often to have code reviewers check the code manually, looking for potential ...

Recommended for you

BPG image format judged awesome versus JPEG

4 hours ago

If these three letters could talk, BPG, they would say something like "Farewell, JPEG." Better Portable Graphics (BPG) is a new image format based on HEVC and supported by browsers with a small Javascript ...

Atari's 'E.T.' game joins Smithsonian collection

Dec 15, 2014

One of the "E.T." Atari game cartridges unearthed this year from a heap of garbage buried deep in the New Mexico desert has been added to the video game history collection at the Smithsonian.

People finding their 'waze' to once-hidden streets

Dec 14, 2014

When the people whose houses hug the narrow warren of streets paralleling the busiest urban freeway in America began to see bumper-to-bumper traffic crawling by their homes a year or so ago, they were baffled.

User comments : 3

Adjust slider to filter visible comments by rank

Display comments: newest first

Eikka
not rated yet Jul 20, 2012
Then the next problem is proofing the hardware itself, e.g. the cache bug in the Intel Atom N270 / Intel Core 2 Duo T5750 processors that basically allows a buffer overrun attack on the machine by letting a specifically crafted program alter arbitrary memory locations if that memory location happens to be cached at the moment.

You'd think that the hardware is engineered to be pretty much perfect, but since these are highly complex systems, you actually can't test them for all possible permutations of inputs and outputs to see if it actually behaves correctly. It would take the life of the universe to do.

It's technically possible to write software too, that you simply cannot predict what it will do until you actually run it, especially if you use self-modifying code, so I kinda doubt that their model is as all-powerful, unless you assume the code already respects the model's limits.
IronhorseA
not rated yet Jul 20, 2012
"You'd think that the hardware is engineered to be pretty much perfect,"

That would be true if the cpu was hardwired, but since most modern cpu's use microcode, similar to firmware in a larger device, then they end up having the same issues as any software. The only positive thing about microcode is that, like assembly language, they're very sensitive to errors in execution, ie. they fail quickly in most cases, giving you the opportunity to fix it before it makes it out of the factory (though not always, as the intel case shows ;P )
tgoldman
not rated yet Jul 20, 2012
This allows coders to choose the benefits of multiple languages, such as using one to ensure portability while using others to enhance performance.

As I recall, this was the goal of an IBM effort called PL1 that was ultimately abandoned.

Please sign in to add a comment. Registration is free, and takes less than a minute. Read more

Click here to reset your password.
Sign in to get notified via email when new comments are made.