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

Andrew munin at mimisbrunnr.net
Wed Jul 9 01:47:25 UTC 2014


It would be nice to see the report also, because perhaps that at least
will say specifically which major branch of PolarSSL was verified. That
security advisory you link only affects the 1.1 branch, while the 1.2
and 1.3 branches are not affected.

On 07/08/2014 09:42 PM, Vitaly Osipov wrote:
> 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