Chapter 6.4. Unsafe Code Audit

We provide three key features for auditing unsafe code:

  • Audit unit generation: Segmenting a Rust crate into multiple code units to examain the correctness of code safety declaration and safety property labeling.
  • Safety property inference: Inferring the safety property of unsafe APIs based on the audit unit.
  • Safety property verification: Verifying if the safety property required by unsafe APIs are satisfied.

Audit Unit Generation

The unsafety propogation graph(UPG) is a novel method to model the essential usage and encapsulation of unsafe code. UPG combines the traditional call graph with unsafe and dataflow information from Rust to capture the use and propagation of unsafe code across the project.

Within the UPG, there contains four major isolation types and nine structural patterns to split a UPG into several small self-contained subgraphs. These subgraphs called unsafety isolation graphs(UIGs) can serve as useful audit units for examining the soundness of unsafe code encapsulation.

We will continue to explore and investigate more effective applications of UIG in the encapsulation of unsafe code in our subsequent research.

Before using this feature, make sure that graphviz is installed on your device.

generate upg

Get into the same directory as cargo.toml and run the cmd below from the teminal. 

cargo rapx -upg

Then 'rapx' will create a directory named 'UPG' in the same level, which contains several connected unsafety propogation graphs.

count uig

This feature is numerically calculated based on the type of all uig in the target crate

cargo rapx -uig

check safety doc

With the following cmd, users can check for unsafe apis that lack an unsafe document annotation

cargo rapx -doc

RAPx will output the corresponding unsafe api information, including its location and visibility level as follows:

Lack of unsafety doc: src/lib.rs:1668:1: 1674:11 (#0), visibility:Restricted(DefId(0:0 ~ smallvec[ecd8])).
Lack of unsafety doc: src/lib.rs:1699:1: 1704:11 (#0), visibility:Restricted(DefId(0:0 ~ smallvec[ecd8])).
Lack of unsafety doc: src/lib.rs:960:5: 960:45 (#0), visibility:Restricted(DefId(0:0 ~ smallvec[ecd8])).

Safety Property Inference

audit unsafe APIs' SP in core and alloc

Specifically, we currently integrate a set of SP labels analysis for core and alloc crate of the Rust standard library.

  1. Create a new helloworld project.
  2. Navigate to the helloworld project directory and run:
cargo rapx -stdsp -- -Z build-std --target x86_64-unknown-linux-gnu > /your/output/log/path/result.log 2>&1

Replace /your/output/log/path with your desired output directory. This will output APIs where the caller and callee have different SPs.

Safety Property Verification