(Press-News.org) Cambridge, Mass – July 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 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."
###
The development of RockSalt was partially funded by Google (although Google researchers were not involved in its development.)
END
A research study led by the Peninsula College of Medicine and Dentistry, University of Exeter, and Boston University School of Medicine, in collaboration with a global consortium, has identified genetic markers that influence a protein involved in regulating oestrogen and testosterone levels in the bloodstream.
The results, published online in PLoS Genetics, also reveal that some of the genetic markers for this protein are near genes related to liver function, metabolism and type 2 diabetes, demonstrating an important genetic connection between the metabolic and reproductive ...
A review article appearing in the July 20, 2012, issue of the journal Science describes groundbreaking discoveries that have emerged from the Relativistic Heavy Ion Collider (RHIC) at the U.S. Department of Energy's Brookhaven National Laboratory, synergies with the heavy-ion program at the Large Hadron Collider (LHC) in Europe, and the compelling questions that will drive this research forward on both sides of the Atlantic. With details that help enlighten our understanding of the hot nuclear matter that permeated the early universe, the article is a prelude to the latest ...
MAYWOOD, Ill. - Caregivers of stroke survivors are at risk for developing depression and complications from chronic stress, according to a study published by researchers at the Loyola University Chicago Marcella Niehoff School of Nursing (MNSON) in the latest issue of Biological Research for Nursing.
Stroke is one of the leading causes of long-term disability, according to the Centers for Disease Control and Prevention. The National Family Caregiver Association reports that up to 80 percent of stroke survivors are cared for by family members who help them manage their ...
It may pay to invest, but it might be worth more to invest in companies that do not have political ties, says one University of Alberta researcher.
Sadok El Ghoul, an associate professor at Campus Saint-Jean, and fellow researchers from the American University of Sharjah and the Olayan School of Business recently presented a paper at the annual conference of the International Journal of Accounting that explored the workings of politically connected firms. In a review of firms from 31 countries, they contend that firms that have some level of political connection, direct ...
UCLA researchers have developed a new transparent solar cell that is an advance toward giving windows in homes and other buildings the ability to generate electricity while still allowing people to see outside. Their study appears in the journal ACS Nano.
The UCLA team describes a new kind of polymer solar cell (PSC) that produces energy by absorbing mainly infrared light, not visible light, making the cells nearly 70% transparent to the human eye. They made the device from a photoactive plastic that converts infrared light into an electrical current.
"These results ...
Severe influenza doubles the odds that a person will develop Parkinson's disease later in life, according to University of British Columbia researchers.
However, the opposite is true for people who contracted a typical case of red measles as children – they are 35 per cent less likely to develop Parkinson's, a nervous system disorder marked by slowness of movement, shaking, stiffness, and in the later stages, loss of balance.
The findings by researchers at UBC's School of Population and Public Health and the Pacific Parkinson's Research Centre, published online this ...
A new study shows that a therapeutic intervention called Cognitively-Based Compassion Training (CBCT) appears to improve the mental and physical health of adolescents in foster care. CBCT is a tool that provides strategies for people to develop more compassionate attitudes toward themselves and others.
It is well documented that children in foster care have a high prevalence of trauma in their lives. For many, circumstances that bring them into the foster care system are formidable -- sexual abuse, parental neglect, family violence, homelessness, and exposure to drugs. ...
The amount of structural damage that radiation causes in electronic materials at the atomic level may be at least ten times greater than previously thought.
That is the surprising result of a new characterization method that uses a combination of lasers and acoustic waves to provide scientists with a capability tantamount to X-ray vision: It allows them to peer through solid materials to pinpoint the size and location of detects buried deep inside with unprecedented precision.
The research, which was conducted by post-doctoral fellow Andrew Steigerwald under the supervision ...
NASA's Aqua satellite has been tracking the remnants of Tropical Depression Khanun, and infrared data revealed that it has moved over northeastern China where it is now dissipating.
NASA's Aqua satellite passed over Khanun on July 18, 19 and 20 and tracked the northeastern progression of the tropical cyclone after it made landfall. On Wednesday, July 18 at 1659 UTC (12:59 p.m. EDT/U.S.), Tropical Depression Khanun's center was still in the Yellow Sea (west of South Korea). At that time, the Atmospheric Infrared Sounder (AIRS) instrument onboard NASA's Aqua satellite saw ...
NASA satellite data has watched cloud temperatures drop in a low pressure system in the western North Pacific Ocean called System 92W, indicating that there's more uplift and power in the storm. That's a sign the storm is strengthening.
Infrared data gathered by NASA's Atmospheric Infrared Sounder (AIRS) instrument indicate cloud top temperatures as well as sea surface temperatures. NASA's Aqua satellite passed over System 92W on July 18, 19 and 20 and watched the low pressure area develop east of the Philippines, organize and move northeast of Luzon, Philippines by July ...
