NASA Jet Propulsion Laboratory (JPL) in Pasadena, California, is the maker of the recent mission to Mars, Curiosity, as well as many previous space missions.
When risk is not an option
Modern space projects require highly specialized software development. The margin for error is so small that software quality assurance procedures are among the most rigorous in the world.
All mission-critical software has to comply with internal, risk-reduction coding standards. Klaus Havelund and Gerard J. Holzmann, leaders of NASA JPL’s Laboratory for Reliable Software (LaRS), its dedicated research team, published a scientific paper explaining the motivations for the software certification implemented at NASA. Quoting from that paper:
“For flight code, JPL has adopted an Institutional Coding Standard with which it requires compliance in all newly developed mission-critical software written at JPL. Except in rare cases, noncompliance is not an option for our flight software developers. Because all rules in the standard are specifically risk related (i.e. we can often point at a mission anomaly or mission loss that was caused by the violation of the underlying principle), approval for non-compliance is also rarely requested or granted. An example of a risk-related rule in this coding standard is the abolition of all dynamic memory use and of recursive code. Some of the motivation for the rules can be traced to the Power of Ten rules.”
The challenge was to find a way to ensure that all mission-critical code complies fully with these coding standards.
Static code analyzers miss a defect
NASA JPL utilizes many commercial static code analyzers for checking code quality. All these solutions were in production use on the Curiosity mission. In February 2012, as Curiosity traveled toward Mars, a JPL engineer discovered a code defect that had gone undetected by the static code analysis of the critical Entry, Descent and Landing software. While this defect was found to have no adverse impact on the functioning of the software, the team realized that similar, more serious, defects might also have been overlooked by the static analysis checks.
Semmle to the rescue with custom-defined defect searches
JPL contacted Semmle for help discovering where other defects might exist in the Curiosity control software. It took just 20 minutes to define a new rule with the Semmle query language (QL) to locate all instances of the defect:
from Function f, FunctionCall c, int i, int a, int b where f = c.getTarget() and a = ((ArrayType)c.getArgument(i).getType()).getArraySize() and b = ((ArrayType)f.getParameter(i).getType()).getArraySize() and a < b select c.getArgument(i), "Array of size " + a + f " passed to $@ passed to $@, which expects an array of size " + b + ".", f, f.getName()
When JPL queried the code that controlled the spacecraft, it quickly identified the original defect and thirty related cases elsewhere in the code. This gave the engineers time to fix the code before the landing – helping to secure a safe touch-down on Mars.
NASA ultimately implemented the rules defining their full Institutional Coding Standard for Java and C in Semmle to perform better static analysis on their code.
- Risk analysis: Semmle gives a comprehensive overview of how well each project compiles with JPL’s custom, risk-reduction, coding standards.
- Targeted resources: JPL uses the detailed insight to prioritize work on rule violations and ensure resources are focused at the point of highest risk.
- Customized solutions: the benefits of Semmle’s fast and fully customizable analysis were brought into sharp relief by the Curiosity project.
- Highly recommended: Gerard Holzmann published a ranked assessment of source code analysis tools on his website placing Semmle at the top.