Featured Research

from universities, journals, and other organizations

Better security for web and mobile applications

Date:
July 20, 2012
Source:
Harvard University
Summary:
When it comes to computer security, who checks the checker? Computer scientists have 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.

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 Google 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 computer scientists 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."


Story Source:

The above story is based on materials provided by Harvard University. Note: Materials may be edited for content and length.


Cite This Page:

Harvard University. "Better security for web and mobile applications." ScienceDaily. ScienceDaily, 20 July 2012. <www.sciencedaily.com/releases/2012/07/120720135707.htm>.
Harvard University. (2012, July 20). Better security for web and mobile applications. ScienceDaily. Retrieved July 28, 2014 from www.sciencedaily.com/releases/2012/07/120720135707.htm
Harvard University. "Better security for web and mobile applications." ScienceDaily. www.sciencedaily.com/releases/2012/07/120720135707.htm (accessed July 28, 2014).

Share This




More Computers & Math News

Monday, July 28, 2014

Featured Research

from universities, journals, and other organizations


Featured Videos

from AP, Reuters, AFP, and other news services

Google's Next Frontier: The Human Body

Google's Next Frontier: The Human Body

Newsy (July 27, 2014) Google is collecting genetic and molecular information to paint a picture of the perfectly healthy human. Video provided by Newsy
Powered by NewsLook.com
Congress OKs Unlocking Phones From Carriers

Congress OKs Unlocking Phones From Carriers

Newsy (July 26, 2014) A bill legalizing "unlocking," or untethering a phone from its default wireless carrier, has passed Congress and is expected to be signed into law. Video provided by Newsy
Powered by NewsLook.com
Apple Acquires 'Pandora of Books' Service BookLamp

Apple Acquires 'Pandora of Books' Service BookLamp

Newsy (July 26, 2014) Apple reportedly acquired analytics and recommendation engine BookLamp for between $10 and $15 million. Video provided by Newsy
Powered by NewsLook.com
Wikipedia Puts Congress in Time Out, Blocks Editing

Wikipedia Puts Congress in Time Out, Blocks Editing

Newsy (July 26, 2014) An IP address within the House of Representatives was banned from editing Wikipedia articles for 10 days after it made some questionable changes. Video provided by Newsy
Powered by NewsLook.com

Search ScienceDaily

Number of stories in archives: 140,361

Find with keyword(s):
Enter a keyword or phrase to search ScienceDaily for related topics and research stories.

Save/Print:
Share:

Breaking News:
from the past week

In Other News

... from NewsDaily.com

Science News

Health News

Environment News

Technology News



Save/Print:
Share:

Free Subscriptions


Get the latest science news with ScienceDaily's free email newsletters, updated daily and weekly. Or view hourly updated newsfeeds in your RSS reader:

Get Social & Mobile


Keep up to date with the latest news from ScienceDaily via social networks and mobile apps:

Have Feedback?


Tell us what you think of ScienceDaily -- we welcome both positive and negative comments. Have any problems using the site? Questions?
Mobile: iPhone Android Web
Follow: Facebook Twitter Google+
Subscribe: RSS Feeds Email Newsletters
Latest Headlines Health & Medicine Mind & Brain Space & Time Matter & Energy Computers & Math Plants & Animals Earth & Climate Fossils & Ruins