DR Checker and KINT static checkers

DR Checker and KINT static checkers

[Dan Carpenter]

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

DR Checker and KINT static checkers

[Dan Carpenter]

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

Re: DR Checker and KINT static checkers

[Julia Lawall]

On Wed, 13 Sep 2017, 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/

I'm always puzzled by statements like:

Some 5,000 warnings were generated, of which nearly 4,000 were verified as
correct by the team. Of those, 158 were actual bugs that were reported
upstream and fixed.

If they took the time to validate 5000 bugs, couldn't they have sent more
patches, or at least made the results public in some way so that other
people could fix them?  Maybe the others are "duplicated, but correct"...

I'm a bit short on time at the moment, but if an outreachy applicant wants
to put together a precise description of how to install and run the tool,
I have plenty of computing power available :)

julia


>
> 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
>
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>

Re: DR Checker and KINT static checkers

[Julia Lawall]

On Wed, 13 Sep 2017, 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/

I'm always puzzled by statements like:

Some 5,000 warnings were generated, of which nearly 4,000 were verified as
correct by the team. Of those, 158 were actual bugs that were reported
upstream and fixed.

If they took the time to validate 5000 bugs, couldn't they have sent more
patches, or at least made the results public in some way so that other
people could fix them?  Maybe the others are "duplicated, but correct"...

I'm a bit short on time at the moment, but if an outreachy applicant wants
to put together a precise description of how to install and run the tool,
I have plenty of computing power available :)

julia


>
> 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
>
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>

Re: DR Checker and KINT static checkers

[Colin Ian King]

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.

Colin

Re: DR Checker and KINT static checkers

[Colin Ian King]

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.

Colin

Re: DR Checker and KINT static checkers

[Julia Lawall]

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

>
> Colin
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>

Re: DR Checker and KINT static checkers

[Julia Lawall]

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

>
> Colin
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>

Re: DR Checker and KINT static checkers

[Colin Ian King]

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

Yep, I'll do that sometime this week when I get some free cycles. :-)

Colin

> 
>>
>> Colin
>> --
>> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
>> the body of a message to majordomo@vger.kernel.org
>> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>>
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> 

Re: DR Checker and KINT static checkers

[Colin Ian King]

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

Yep, I'll do that sometime this week when I get some free cycles. :-)

Colin

> 
>>
>> Colin
>> --
>> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
>> the body of a message to majordomo@vger.kernel.org
>> More majordomo info at  http://vger.kernel.org/majordomo-info.html
>>
> --
> To unsubscribe from this list: send the line "unsubscribe kernel-janitors" in
> the body of a message to majordomo@vger.kernel.org
> More majordomo info at  http://vger.kernel.org/majordomo-info.html
> 

Re: DR Checker and KINT static checkers

[Dan Carpenter]

On Wed, Sep 13, 2017 at 12:01:33PM +0200, Julia Lawall wrote:
> 
> On Wed, 13 Sep 2017, 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/
> 
> I'm always puzzled by statements like:
> 
> Some 5,000 warnings were generated, of which nearly 4,000 were verified as
> correct by the team. Of those, 158 were actual bugs that were reported
> upstream and fixed.

My read was that the 4000 warnings were code bugs that don't affect
runtime, such as inconsistent NULL checking but the pointer isn't
NULL so it doesn't affect runtime?  That's a pure guess.

> 
> If they took the time to validate 5000 bugs, couldn't they have sent more
> patches, or at least made the results public in some way so that other
> people could fix them?  Maybe the others are "duplicated, but correct"...

I think people are worried about posting the results so they don't get
blamed for disclosing a kernel vulnerability.  I used to worry about
that but now I assume everything a static checker can find is public
information already.

regards,
dan carpenter

Re: DR Checker and KINT static checkers

[Dan Carpenter]

On Wed, Sep 13, 2017 at 12:01:33PM +0200, Julia Lawall wrote:
> 
> On Wed, 13 Sep 2017, 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/
> 
> I'm always puzzled by statements like:
> 
> Some 5,000 warnings were generated, of which nearly 4,000 were verified as
> correct by the team. Of those, 158 were actual bugs that were reported
> upstream and fixed.

My read was that the 4000 warnings were code bugs that don't affect
runtime, such as inconsistent NULL checking but the pointer isn't
NULL so it doesn't affect runtime?  That's a pure guess.

> 
> If they took the time to validate 5000 bugs, couldn't they have sent more
> patches, or at least made the results public in some way so that other
> people could fix them?  Maybe the others are "duplicated, but correct"...

I think people are worried about posting the results so they don't get
blamed for disclosing a kernel vulnerability.  I used to worry about
that but now I assume everything a static checker can find is public
information already.

regards,
dan carpenter

Re: DR Checker and KINT static checkers

[Colin Ian King]

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

Re: DR Checker and KINT static checkers

[Colin Ian King]

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