<div dir="ltr">Has anybody seen the new verified C compiler that came out of inria? I think it's supposed to show that if it does not give a warning, that there can be no segfault. But I'm not sure about leakage and other concerns.</div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Aug 18, 2015 at 11:01 AM, Victor Rodriguez <span dir="ltr"><<a href="mailto:vm.rod25@gmail.com" target="_blank">vm.rod25@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">+1 to coverity we use that :)<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
On Tue, Aug 18, 2015 at 9:01 AM, leo kirotawa <<a href="mailto:kirotawa@gmail.com">kirotawa@gmail.com</a>> wrote:<br>
> For memory leaks kernel has a clever mechanism to verify it that you<br>
> can enable in .config for use [1].<br>
> You can also uses Sparse in kernel for static analyze purpose.<br>
><br>
> There are others out there such as coverity scan, coccinelle, etc.<br>
><br>
> [1] <a href="https://www.kernel.org/doc/Documentation/kmemleak.txt" rel="noreferrer" target="_blank">https://www.kernel.org/doc/Documentation/kmemleak.txt</a><br>
><br>
> []'s<br>
><br>
><br>
> On Tue, Aug 18, 2015 at 10:45 AM, Kenneth Adam Miller<br>
> <<a href="mailto:kennethadammiller@gmail.com">kennethadammiller@gmail.com</a>> wrote:<br>
>> Why? That's what the vast majority of the kernel is written in (besides<br>
>> assembler, but what I'm looking for isn't a way to write safe assembler).<br>
>> Plus, tons of people in the kernel development community *must* have some<br>
>> concern or interest in security. I don't care if the kernel is written in C,<br>
>> but I sure would like my kernel module to be safer. If I can get it I don't<br>
>> care what language it's in-it just has to work and *be secure*.<br>
>><br>
>> On Tue, Aug 18, 2015 at 9:40 AM, Robert P. J. Day <<a href="mailto:rpjday@crashcourse.ca">rpjday@crashcourse.ca</a>><br>
>> wrote:<br>
>>><br>
>>> On Tue, 18 Aug 2015, Kenneth Adam Miller wrote:<br>
>>><br>
>>> > Ok- so I know that C is the defacto standard for kernel<br>
>>> > development...<br>
>>><br>
>>> and that's probably where you should have stopped typing. :-)<br>
>>><br>
>>> rday<br>
>>><br>
>>> --<br>
>>><br>
>>> ========================================================================<br>
>>> Robert P. J. Day Ottawa, Ontario, CANADA<br>
>>> <a href="http://crashcourse.ca" rel="noreferrer" target="_blank">http://crashcourse.ca</a><br>
>>><br>
>>> Twitter: <a href="http://twitter.com/rpjday" rel="noreferrer" target="_blank">http://twitter.com/rpjday</a><br>
>>> LinkedIn: <a href="http://ca.linkedin.com/in/rpjday" rel="noreferrer" target="_blank">http://ca.linkedin.com/in/rpjday</a><br>
>>> ========================================================================<br>
>>><br>
>><br>
>><br>
>> _______________________________________________<br>
>> Kernelnewbies mailing list<br>
>> <a href="mailto:Kernelnewbies@kernelnewbies.org">Kernelnewbies@kernelnewbies.org</a><br>
>> <a href="http://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies" rel="noreferrer" target="_blank">http://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies</a><br>
>><br>
><br>
><br>
><br>
> --<br>
><br>
> ----------------------------------------------<br>
> Leônidas S. Barbosa (Kirotawa)<br>
> blog: <a href="http://corecode.wordpress.com" rel="noreferrer" target="_blank">corecode.wordpress.com</a><br>
><br>
> _______________________________________________<br>
> Kernelnewbies mailing list<br>
> <a href="mailto:Kernelnewbies@kernelnewbies.org">Kernelnewbies@kernelnewbies.org</a><br>
> <a href="http://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies" rel="noreferrer" target="_blank">http://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies</a><br>
</div></div></blockquote></div><br></div>