Lightweight type analysis for memory safety through verification of API uses

Lightweight type analysis for memory safety through verification of API uses

[Marcelo Sousa]

(* Apologies if this is a duplicate: I screw up the plain text before *)

Hello all,

I've designed and implemented a tool similar to sparse and CQUAL that
does type inference of user specified type qualifiers, e.g. iomem. It
receives an API specification with the type qualifiers and also a
partial order, e.g. IOAddr is not compatible with KernelAddr and
ioremap returns a pointer to IOAddr while __kmalloc returns a pointer
to a KernelAddr.

The tool is part of a verification framework for LLVM that I'm
developing called llvmvf. I'm using the llvmlinux project to compile
with clang and I perform intra/interprocedural analysis on every IR
module. I can easily extend to inter-module analysis for a whole
driver analysis.

The performance results are quite fast when compared to similar tools:
less than 5 min to analyse the entire source code (~9k modules;
millions of constraints).

Initially, I focused on separation of IO vs regular memory and I
implemented a partial transformation that converts inline assembly to
LLVM IR functions because I'm also interested in catching misuses of
atomic instructions with IO memory pointers.

I'm looking for bugs related to misuses of IO pointers to validate my
approach and have a good direction on how to increase the precision.
More importantly, I'm looking for other use cases that are likely to
produce a small number of false positives and could be useful to the
linux kernel community. I would like your general feedback and
suggestions of analysis. In particular, I'm thinking on using this
approach to verify the DMA API, and I'm looking for known bugs that
could be used for validation.

Kind regards,
Marcelo

Re: Lightweight type analysis for memory safety through verification of API uses

[Andi Kleen]

Marcelo Sousa <marceloabsousa@gmail.com> writes:

> I've designed and implemented a tool similar to sparse and CQUAL that
> does type inference of user specified type qualifiers, e.g. iomem. It
> receives an API specification with the type qualifiers and also a
> partial order, e.g. IOAddr is not compatible with KernelAddr and
> ioremap returns a pointer to IOAddr while __kmalloc returns a pointer
> to a KernelAddr.

Tracking iomem is ultimatively not very interesting, as in many common
architectures it's just a normal pointer.

__user is much more interesting, as that is real security bugs.
You can probably find some in standard security advisories.

Really interesting would be static lock set tracking for pointers
and similar.

-Andi

-- 
ak@linux.intel.com -- Speaking for myself only

Re: Lightweight type analysis for memory safety through verification of API uses

[Marcelo Sousa]

Dear Andi,

Thanks for the reply.

On Tue, Sep 24, 2013 at 5:11 AM, Andi Kleen <andi@firstfloor.org> wrote:
> Marcelo Sousa <marceloabsousa@gmail.com> writes:
>
>> I've designed and implemented a tool similar to sparse and CQUAL that
>> does type inference of user specified type qualifiers, e.g. iomem. It
>> receives an API specification with the type qualifiers and also a
>> partial order, e.g. IOAddr is not compatible with KernelAddr and
>> ioremap returns a pointer to IOAddr while __kmalloc returns a pointer
>> to a KernelAddr.
>
> Tracking iomem is ultimatively not very interesting, as in many common
> architectures it's just a normal pointer.

My motivation for tracking iomem was the fact that cmpxchg in x86 had
the side effect of always writing to the memory pointer even if the
comparison fails. Since the iomem pointer could be pointing to a
non-readable location performing a cmpxchg would always result in
memory corruption.

>
> __user is much more interesting, as that is real security bugs.
> You can probably find some in standard security advisories.

Yes, there has been research on user vs kernel pointer separation, and
I'm focusing on that at the moment. However, I can't really find any
recent bugs on this topic. If you can provide pointers that would be
great.

>
> Really interesting would be static lock set tracking for pointers
> and similar.

Is this to track that lock/unlock is correctly modelled (no double
lock, no unlock before lock, deadlock) or do you have a specific goal
in mind? Again, if you know of any existing bugs or a particular
pattern that you are interested in verifying that would be great.

Kind regards,
Marcelo

>
> -Andi
>
> --
> ak@linux.intel.com -- Speaking for myself only