Project Overview
This is a brief overview of our project. For a more detailed presentation of our project, click here.
Our project centers around L-SAP, a program analysis tool for Eclipse. It is used to perform scalable
and accurate lock/unlock pairing analysis for the Linux Kernel. L-SAP performs a model-based verification
(with the help of Atlas) to transform the many paths of the linux codebase into graph models that can
be analyzed and verfied for lock/unlock pairs. If L-SAP is unable to perform a conclusive analysis,
human readable graphs are created as evidence and a manual verification process of that locking instance
can be performed.
The Problem
L-SAP is a great tool that has already discovered numerous lock/unlock mismatches, leading to a better
more secure kernel. However, there are a number of steps that must be performed every time the kernel is tested:
- Create an L-SAP Patch to get the Kernel ready for L-SAP
- Run the verifier
- Post the results on a public website
While these steps don't seem like a lot of work, they are tedious to do manually. The Patch for L-SAP
simply redirects all the lock/unlock methods in the kernel to a single dummy function. Since this
version of the kernel will never be run, funnelling all locking methods to a dummy lock method and
all unlock methods to a dummy unlock method makes L-SAP run quicker and efficient. However, creating
this patch for every version requires an understanding of which lock/unlock methods exist and making
sure their definitions have not changed.
Running the verifier takes time and is very memory intensive. While the verifier can be run automatically,
The results it generates do map back to previous versions of the kernel. This means there is no way to
check the difference between the same instance in two versions of the kernel.
Finally, the results of the verifier get packaged into an antiquated website design. This design makes
it hard to find a specific instance and once the instance is found, there is no clear cut information
as to the final status of the verifier.
The Solution
Our Solution to the problems of the L-SAP Verifier Pipeline aims to automate the entire verifier process.
In this way, the setup of L-SAP can be made faster and can happen as soon as a new version of Linux
is released.
We plan to do this by segmenting the pipeline into 4 different modules and automating each part:
- Patch Creation and Application
- Difference Mapping and Running L-SAP
- Difference Summarization
- Posting Results to the Website
Since each step is modular, they were all developed simultaneously. Patch Creation is handled
automatically and an algorithm analyzing lock/unlock methods is used to automatically create new
patches and apply them to the new version of the kernel.
A new difference mapping algorithm is applied to the previous version of the kernel and is
used to map previous version's instances to the new version's instances. L-SAP then runs
and the results are passed to the difference linker. A difference summary is prepared using the map generated before L-SAP was run. This allows
viewers to see only the instances that changed between versions.
Finally, all the results are posted to a new website. The new website includes a much
needed search and filtering tool, allowing viewers to pinpoint the instance they are looking for. They
are also able to clearly tell the status of the instance looking at the detail page.
More Information
To see the final website design, click here
For more information on L-SAP, click here
For a detailed description on our project, check out our design documents or view a presentation
on our solution here.
