An Automated Analysis of Safety and Security in the Drake System

This document presents the results of running Petablox and other state-of-the-art automated static analysis tools on the Drake codebase to uncover safety and security issues. We present analytics results for various Drake modules, describe potential issues we discovered, provide pointers to raw output of the tools, and outline future directions to improve the tools.

The Checkers

We ran various checkers in four different automated static analysis tools on the Drake codebase obtained from http://drake.mit.edu/from_source.html

1. Petablox: API misuse checkers (http://www.seas.upenn.edu/~mhnaik/papers/sec16.pdf)
2. FB Infer: Memory safety checkers (http://FBinfer.com)
3. MIT Kint: Integer overflow checker (http://css.csail.mit.edu/kint)
4. Coverity: bug pattern checkers (https://scan.coverity.com)

We present the results of only Petablox and FB Infer. Kint reported problems compiling Drake that are easy but tedious to fix. Coverity is not free to download but it is available as a free service for github hosted projects (such as Drake); its results will be available at a later date.

Key Findings

• Petablox and FB Infer were able to run successfully on 2.1M lines of source code (1.97M lines of Drake externals plus 138K lines of Drake core). This attests to the suitability of these tools for analyzing large and complex autonomous software systems.
• Petablox found 1 performance bug, 2 buffer underrun bugs and 9 null dereference bugs, and FB Infer found 138 potential null dereference bugs. Among these, four representative alarms are as follows.

  Link to details	High-level description
  Null Dereference in externals/ipopt	A pointer is allocated memory depending on a condition. But the condition may not hold when the pointer is accessed.
  Null Dereference in drake/multibody	A xml attribute value is retrieved and used. If the attribute does not exist, null dereference can occur. By testing, we confirmed it causes a crash.
  Buffer Underrun in externals/ipopt	An integer element is retrieved from a priority queue and used as index of a buffer. If the queue is empty, the index can be -1.
  PERF in drake/multibody	The C++ idiom "move" to avoid unnecessary copies is not used at a point whereas it is almost always used throughout the code.

Checker Analytics

Modules	Petablox	FBInfer
drake/automotive	0	22
drake/multibody	559	1
drake/systems	1203	13
drake/common	1008	2
externals/libbot	38	108
externals/ipopt	13	70

Analysis Results

Our analysis of potential safety/security issues discovered in Drake by the tools is available in files under directory analysis_results.

Detailed Output

The raw output of running the tools on Drake is available in folders under directory raw_logs.