About Atlas

Atlas is a state-of-the-art platform for building fast, highly-scalable solutions to software analysis problems. Atlas has been used to analyze large-legacy software ranging in tens of millions of lines of code. Application areas include automatic porting, binary analysis, malware detection, and minimal patch generation. EnSoft has used Atlas to build custom solutions for the US Department of Defense, as well as commercial clients.

Atlas is a platform for software analysis using graph schema. Below, we will demonstrate how to check a memory safety property using Atlas.

The code shown to the right is from XINU, an embedded operating system. In the function dswrite, a memory is allocated on line 21 using the function getbuf. But a corresponding deallocation, using the function freebuf in XINU, is missing. When an allocated memory is not deallocated, it is a memory safety violation and is called memory leak. Is there a memory leak in XINU?

Static analysis tools perform inter-procedural analysis to compute the call chains on screen and find that on some execution paths, the memory is deallocated in the function dskqopt but not on all execution paths. Thus, the tools conclude there is a memory leak in XINU and recommend deallocating memory at the end of dswrite. This fix is problematic as it violates the XINU design, which takes care of the issue using interrupts. A correct analysis should also capture a function which is invoked by an interrupt and deallocates the memory. This is a valid implementation of the producer-consumer pattern and there is in fact no memory leak. Let’s dive in and find this missing function using Atlas.

Analysis in Atlas is done by interacting with the graph representation. Atlas provides a query language to facilitate the interaction and an execution environment to execute the queries. This environment is called the Atlas Shell. You can open the Atlas Shell by clicking Atlas -> Open Atlas Shell. Let’s warm up by locating the code we are interested in: the function dswrite. 

The query for locating dswrite is (functions query). Hit enter to execute the query. Using the show query we can see the result of the executed query. It shows a node in the graph that represents the function dswrite. Atlas maintains source-correspondence with the graph. Double-clicking on the graph elements navigates to the code segments represented by the graph elements.

The function dswrite allocates a memory of the type dreq. We will make use of this information to discover the missing function necessary to complete the analysis.

Let’s start by creating some handy variables to represent the allocation function getbuf, the deallocation function freebuf, and the type dreq.

First compute all the functions that can potentially alias the memory allocated in dswrite. Let’s see the result of the query. It does capture dswrite as expected but it also captures dsinter, the function invoked by an interrupt. We are interested in a subset of these functions as not all of them can deallocate the memory.

The query to compute the relevant functions and the call chains is a combination of multiple queries. The first query computes the relevant call chains originating at dswrite. The second query computes the relevant call chains invoked by an interrupt. Finally, we combine the two results.

Here are the call chains computed by the query that are necessary to complete the analysis . It shows that dswrite allocates a memory, which is passed through dskenq to dskqopt and is deallocated on some execution paths in dskqopt. The other mechanism for deallocation is via dsinter, which is invoked by an interrupt. It accesses the memory allocated in dswrite using a global alias and deallocates it. The verification can then be completed using a model checker to verify all execution paths captured in these call chains.