Semmle at NASA: Landing Curiosity safely on Mars
In creating technology for NASA JPL’s space and planetary exploration missions, the NASA JPL team relies on Semmle to spot and eliminate mission-critical code problems, such as the crashing bug that could have ended the Curiosity Rovers mission before it had begun.
From Explorer 1 to the ongoing Mars expeditions, NASA’s Jet Propulsion Laboratory is responsible for many of the most famous and celebrated space and planetary exploration missions the world has seen.
Modern space exploration projects require highly specialized software development that works in unison with the custom-made hardware that is built and optimized for each individual space project. Even the smallest flaw in the JPL software can cause the hardware to malfunction or behave unexpectedly, ultimately causing the mission to go up in smoke.
With hundreds of millions of taxpayer dollars invested in each mission, and groundbreaking scientific endeavors at stake, NASA space missions have no margin for error. Consequently, NASA JPL’s testing process for software is among the most demanding in the world, with extensive standards and rules to be followed without exception by the flight software developers who create the mission software.
JPL have good reason for a strict enforcement of their extensive coding standards. Klaus Havelund and Gerard J. Holzmann, leaders of NASA JPL’s Laboratory for Reliable Software (LaRS) at the time of Curiosity’s travel towards Mars, published a paper explaining the motivations for the stringent software certification implemented at NASA. In their paper they write:
We can often point at a mission anomaly or mission loss that was caused by the violation of the underlying principle
Despite rigorous testing and reviewing, serious bugs may surface:
When the Curiosity Rover was on its way to Mars in 2012, a flight software developer at NASA JPL discovered a mission-critical bug through manual code review. The problem occurred in Curiosity’s Entry, Descent and Landing software - the software responsible for the rovers descent through the Martian atmosphere and landing it safely on surface of Mars.
The bug, which had gone undetected by traditional solutions, was likely to prevent the capsule’s parachutes from opening, resulting in the Rover crashing onto the red planet’s rocky surface.
The problem stems from a peculiarity of the C language that allows you to declare parameters to have array types (with stated sizes), but that means nothing: the parameter type degrades to a raw pointer type with no size information.
The pseudo code illustrates the problem. The function is declared to take an array of length 12. However, there’s no sanity checking, and a developer might call it with an array that’s too short, holding direction information for only one of the thrusters. The function will then read past the end of the array, and unpredictable results occur.
Patching is still possible mid-flight, but patching the problem would not guarantee the mission. The team needed to know if any variants of the problem existed other places in the code.
A while before Curiosity left Planet Earth, Havelund and Holzmann got acquainted with Semmle. They did a thorough assessment of Semmle QL and recognized the value of creating custom analyses to identify variants and implement NASA’s coding standards, and as a result, NASA partnered with Semmle. This soon proved to be of great value to the agency.
Once the mission critical bug was discovered on the Curiosity, JPL contacted Semmle for help discovering whether variants of the problem might exist in the Curiosity control software.
In 20 minutes, research engineers from Semmle produced a QL query and shared it with the JPL team.
QL query that find the original problem, along with more than30 variants.
Complete text of analysis.
The JPL team ran the query across the full Curiosity control software, and it identified the original problem, and more than 30 other variants, of which three were in the critical Entry, Descent and Landing module.
The team addressed all issues, and patched the firmware remotely. Not long after, the Curiosity Rover landed safely on Mars.
NASA JPL are using Semmle QL throughout the organization to enforce NASA’s coding standards, to find and eradicate critical software problems and their variants, as well as Semmle LGTM to effectively share best practices and knowledge across the team of NASA JPL’s flight software developers and to prevent variants of known problems from ever being introduced into mission software.
NASA JPL’s partnership with Semmle has proven to make a big difference to the missions - helping to ensure a safe landing for the Curiosity rover on Mars, and secure the JPL software for future missions.