Tooling to Detect Unwanted Thread Exits in Rust

Abstract

Technolution is a company that specializes in building embedded and information systems, in which software plays a key role. Recently, Technolution is transitioning from the use of C in embedded systems, to Rust, a relatively new programming language developed by Mozilla. By design, Rust provides the programmer with higher security and reliability guarantees, such as memory safety, type safety and the absence of race conditions. These guarantees are ensured by means of an expressive ownership-based type system. However, it is impossible for the Rust type system to detect all errors statically. Hence, there are still many operations that contain dynamic checks to test for erroneous conditions. When such a check fails, an unrecoverable problem has been encountered and the current thread exits, this is called a panic in Rust. A panic causes the program to terminate, leading to a decrease in availability of the system. To avoid situations causing panic, Technolution wants tooling that detects possible ways a program could panic. For this purpose, we developed a static analysis tool: Rustig. When given a program, Rustig notifies the user of all the operations that either directly, or indirectly via another library, may cause a panic. The tools performs the analysis of panic calls in two stages. First, it builds a call graph from the executable of a Rust program, modelling functions as nodes and function calls as directed edges. Secondly, it performs an analysis on the call graph to determine which functions could cause panic. As part of the development of Rustig, we devised two new approaches. We have developed an approach to construct call graphs taking into account dynamic dispatch calls. This is based upon the assumption once a function address is loaded, it will also be called during execution. Furthermore, in order to efficiently analyze the call graph, a simplification of the all paths problem is proposed. In contrast with the all paths problem, the simplification is solvable in polynomial time. The approach involves finding the shortest path for every crossing edge on a graph cut.