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

Andrew munin at mimisbrunnr.net
Wed Jul 9 01:06:38 UTC 2014


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
> 
> 


More information about the langsec-discuss mailing list