Safety Hole Analyzer

Safety holes

This section describes the analysis of the Linux kernel to infer preconditions for triggering safety holes in kernel exported functions. We describe here some of the main semantic matches that implement the analysis for detecting categories of safety holes. These categories build on the findings of previous work by Chou et al. and Palix et al.

1. Prototype tool

The analysis of the Linux kernel are implemented with SmPL rules, using the Coccinelle program matching and transformation engine.

2. Details on safety hole categories

The safety holes that we focus on belong to various categories dealing with pointer dereference, critical sections, irq management, memory allocation, data exchange between user and kernel spaces.

Each of these categories is divided into into an Entry and an Exit safety hole, to better differentiate two instances of safety holes :

  • entry : the safety hole is triggered in the code of the exported function when the calling code does not respect some given precondition.

  • exit : the exported function finishes its execution but has activated a safety hole that can be triggered after returning to the calling code.

NULL, IsNULL
Do not double-acquire locks Check potentially NULL pointers returned from routines. A test showing that a pointer is NULL is followed by a dereference of that pointer.

  • entry : An exported function dereferences one of its parameter with no prior checks.

  • exit : An exported function returns NULL.

Tip We have augmented this category by writing analysis rules for a more complex case where the invalidity of dereferenced pointer is indirectly related to the invalidity of a parameter of the exported function. For the exit safety hole, we also extend the analysis to another widespread error return value : ERR_PTR.
Note

  • Search for exported functions that possibly/certainlydereference a parameter directly in their body with the direct_deref semantic match.

  • Search for those that may transfer their parameters to internal functions which then performs the dereference, using the differed_deref semantic match. We rely on this ocaml code to perform recursive iterations on all internal functions.

  • In the subtle_deref semantic match, the validity of the dereferenced pointer somehow depends on the validity of a parameter.

  • Exported functions that may return an invalid pointer, i.e, NULL or ERR_PTR whose dereference will be a fault, are collected with the return_null semantic match. The analysis on this case also iterates on all functions internally called by the exported function.
Double Lock, Intr, LockIntr
Do not double-acquire locks

  • entry : An exported function disables interrupts or acquires a lock that is derived from a parameter

  • exit : An exported function returns while holding a lock it has acquired or after disabling interrupts.

Tip We have augmented the entry safety hole by also searching for exported functions that suppose the lock is held and therefore attempt to release it. This analysis rule is based on report of real bug in in-kernel code.
Note

  • Search for exported functions that may acquire a lock derived from a parameter, or that, first, attempt to release a lock.

  • To collect exported functions that present a lock/intr exit safety hole, different cases exist :

    • The function may return while holding a lock it has acquired.

    • The function returns after disabling interrupts. The relevant interrupt management primitives are :

      • primitives that do not accept arguments (cli and local_irq_disable). See the relevant semantic match here.

      • primitves that take arguments (local_irq_save and save_and_cli). See the semantic match here.

      • primitives that take locks and disable interrupts at once.
Block
To avoid deadlock, do not call blocking functions with interrupts disabled or a spinlock held.

  • entry : An exported function calls a blocking function.

  • exit : An exported function disables interrupts and returns without reenabling them

Note

  • Search for functions that may block using a semantic match detecting, for example, allocations function that are called with the GFP_KERNEL flag, and iterating over all API functions.
Free
Do not use freed memory

  • entry : An exported functon dereferences a value derived from a parameter.

  • exit : An exported function frees memory derived from a parameter

Note

  • Search for exported functions that may call kfree on a pointer derived from a parameter. See the semantic patch here. This function follows the exported function parameters as they are passed over to internal APIs, using this ocaml code.