[langsec-discuss] LZO, subtle bugs, theorem provers

Vitaly Osipov vitaly.osipov at gmail.com
Wed Jul 9 01:42:06 UTC 2014


There are always assumptions in all verification projects, presumably
the report spells them out.

It is interesting that PolarSSL still get vulnerabilities from time to
time, e.g. a buffer overflow
https://polarssl.org/tech-updates/security-advisories/polarssl-security-advisory-2013-04
despite claiming being "immune to CWE 119".
Regards,
Vitaly


On Wed, Jul 9, 2014 at 11:06 AM, Andrew <munin at mimisbrunnr.net> wrote:
> I'd like to get a copy of their "PolarSSL Verification Kit" but it seems
> to be hidden behind a "pay us" link. However, what I am able to read
> from the authors so far the answers seems to be:
>
> a. all of it
> b. none of it
>
> I'd love to see more information of course and ideally see the analysis
> run myself. It definitely sounded like they spent a lot of work doing
> modeling / precondition specification as well as analysis tuning to
> verify PolarSSL, which sounds like a lot of work. However, they did it,
> and apparently without re-writing PolarSSL, so...
>
> On 07/08/2014 09:00 PM, Thomas Dullien wrote:
>> Please check up on a) how much of the code is formally verified and b)
>> how much
>> of the code was rewritten to make that feasible :-)
>>
>> Nobody is saying you can't write checkable code. All I am saying that
>> for most / all
>> of our legacy code, making it checkable is equivalent to rewriting it.
>>
>> Cheers,
>> Thomas/Halvar
>>
>>
>> On Tue, Jul 8, 2014 at 5:49 PM, Andrew <munin at mimisbrunnr.net
>> <mailto:munin at mimisbrunnr.net>> wrote:
>>
>>     How does all of this pessimism about the application of static analysis
>>     and formal methods applied to legacy code square with the existence of a
>>     formally verified SSL/TLS stack written in C?
>>
>>     http://www.pl-enthusiast.net/?p=184#comment-96
>>
>>     http://trust-in-soft.com/polarssl-verification-kit/
>>
>>     On 07/08/2014 12:26 AM, Peter Johnson wrote:
>>     >> It seems likely then that verification only works on the subset of
>>     >> expressiveness that can be cowritten in the free and the constrained
>>     >> language.  i.e. we aren't verifying c at all.
>>     >
>>     > Isn't this a direct consequence of C being Turing-complete and
>>     therefore not
>>     > verifiable in the general case?  That is, we know C gives you more
>>     than enough
>>     > rope to hang yourself with and therefore we want to encourage
>>     people to use C
>>     > in ways that are explicitly verifiable.  To me, you've concisely
>>     summed up
>>     > exactly what (I think) LangSec is all about!
>>     >
>>     > pete
>>     >
>>     > _______________________________________________
>>     > langsec-discuss mailing list
>>     > langsec-discuss at mail.langsec.org
>>     <mailto:langsec-discuss at mail.langsec.org>
>>     > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
>>     >
>>     _______________________________________________
>>     langsec-discuss mailing list
>>     langsec-discuss at mail.langsec.org
>>     <mailto:langsec-discuss at mail.langsec.org>
>>     https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
>>
>>
> _______________________________________________
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss


More information about the langsec-discuss mailing list