From: Colin Ian King <colin.king@canonical.com>
To: kernel-janitors@vger.kernel.org
Subject: Re: DR Checker and KINT static checkers
Date: Thu, 14 Sep 2017 17:13:46 +0000 [thread overview]
Message-ID: <114caf1f-c78d-b8ee-7f7e-53625867299c@canonical.com> (raw)
In-Reply-To: <20170913095202.a6zsi3xeryzhmxrl@mwanda>
On 13/09/17 11:04, Julia Lawall wrote:
>
>
> On Wed, 13 Sep 2017, Colin Ian King wrote:
>
>> On 13/09/17 10:52, Dan Carpenter wrote:
>>> LWN.net recently had an article about Dr Checker. It's a promising new
>>> static analysis tool. The LWN article is for subscribers only until
>>> tomorrow, but anyone can read the PDF or install the code. It would be
>>> really interesting if someone could run Dr Checker on a mainline kernel
>>> tree and post the results.
>>> https://lwn.net/Articles/733056/
>>> https://www.usenix.org/system/files/conference/usenixsecurity17/sec17-machiry.pdf
>>> https://github.com/ucsb-seclab/dr_checker/
>>>
>>> The other tool that's quite interesting is KINT which looks for integer
>>> overflows. It's a bit of a pain because you have to annotate some
>>> kernel functions to make it work. The PDF and source code are here:
>>>
>>> http://css.csail.mit.edu/kint/
>>>
>>> regards,
>>> dan carpenter
>>>
>>
>> Funnily enough, I tried Dr Checker out earlier this week. One has to
>> make it do a fake build of the kernel to gather information on how to
>> build the specific kernel config (e.g. how it was compiled and the gcc
>> build flags) and then this gets parsed by DR-Checker. Unfortunately it
>> seems that it only supported arm architecture builds and it could not
>> handle the gcc output for a modern x86 amd64 gcc (gcc 7.2). I kind of
>> gave up after a couple of hours trying to make it work. I suspect more
>> patient developers may figure out how to make it work. I may go back and
>> revisit this when I have some free time.
>
> You could ask the authors. They may be happy to have some feedback.
>
> julia
>
I've requested assistance from Aravind Machiry and he will help me with
x86 checking once he's finished a paper, so I expect to report back with
my results sometime at the end of the month if all goes well. Keep you
posted.
Colin
WARNING: multiple messages have this Message-ID (diff)
From: Colin Ian King <colin.king@canonical.com>
To: Julia Lawall <julia.lawall@lip6.fr>
Cc: Dan Carpenter <dan.carpenter@oracle.com>,
kernel-janitors@vger.kernel.org,
outreachy-kernel@googlegroups.com,
Christophe JAILLET <christophe.jaillet@wanadoo.fr>
Subject: Re: DR Checker and KINT static checkers
Date: Thu, 14 Sep 2017 18:13:46 +0100 [thread overview]
Message-ID: <114caf1f-c78d-b8ee-7f7e-53625867299c@canonical.com> (raw)
In-Reply-To: <alpine.DEB.2.20.1709131203520.13908@hadrien>
On 13/09/17 11:04, Julia Lawall wrote:
>
>
> On Wed, 13 Sep 2017, Colin Ian King wrote:
>
>> On 13/09/17 10:52, Dan Carpenter wrote:
>>> LWN.net recently had an article about Dr Checker. It's a promising new
>>> static analysis tool. The LWN article is for subscribers only until
>>> tomorrow, but anyone can read the PDF or install the code. It would be
>>> really interesting if someone could run Dr Checker on a mainline kernel
>>> tree and post the results.
>>> https://lwn.net/Articles/733056/
>>> https://www.usenix.org/system/files/conference/usenixsecurity17/sec17-machiry.pdf
>>> https://github.com/ucsb-seclab/dr_checker/
>>>
>>> The other tool that's quite interesting is KINT which looks for integer
>>> overflows. It's a bit of a pain because you have to annotate some
>>> kernel functions to make it work. The PDF and source code are here:
>>>
>>> http://css.csail.mit.edu/kint/
>>>
>>> regards,
>>> dan carpenter
>>>
>>
>> Funnily enough, I tried Dr Checker out earlier this week. One has to
>> make it do a fake build of the kernel to gather information on how to
>> build the specific kernel config (e.g. how it was compiled and the gcc
>> build flags) and then this gets parsed by DR-Checker. Unfortunately it
>> seems that it only supported arm architecture builds and it could not
>> handle the gcc output for a modern x86 amd64 gcc (gcc 7.2). I kind of
>> gave up after a couple of hours trying to make it work. I suspect more
>> patient developers may figure out how to make it work. I may go back and
>> revisit this when I have some free time.
>
> You could ask the authors. They may be happy to have some feedback.
>
> julia
>
I've requested assistance from Aravind Machiry and he will help me with
x86 checking once he's finished a paper, so I expect to report back with
my results sometime at the end of the month if all goes well. Keep you
posted.
Colin
next prev parent reply other threads:[~2017-09-14 17:13 UTC|newest]
Thread overview: 14+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-09-13 9:52 DR Checker and KINT static checkers Dan Carpenter
2017-09-13 9:52 ` Dan Carpenter
2017-09-13 10:01 ` Julia Lawall
2017-09-13 10:01 ` Julia Lawall
2017-09-13 10:02 ` Colin Ian King
2017-09-13 10:02 ` Colin Ian King
2017-09-13 10:04 ` Julia Lawall
2017-09-13 10:04 ` Julia Lawall
2017-09-13 10:05 ` Colin Ian King
2017-09-13 10:05 ` Colin Ian King
2017-09-13 10:21 ` Dan Carpenter
2017-09-13 10:21 ` Dan Carpenter
2017-09-14 17:13 ` Colin Ian King [this message]
2017-09-14 17:13 ` Colin Ian King
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=114caf1f-c78d-b8ee-7f7e-53625867299c@canonical.com \
--to=colin.king@canonical.com \
--cc=kernel-janitors@vger.kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.