3 ms·

The work you have been doing on polarssl is pretty inspiring. I use it as a success story for formal methods and PL technology when I do "science of security" c

by munin 11y ago

The work you have been doing on polarssl is pretty inspiring. I use it as a success story for formal methods and PL technology when I do "science of security" classes or briefings. Someday, I would love to do a research project on using tools like yours to prove higher level properties of programs, much like what the Ironclad/Dafny teams have done. Their approach is good when you have a formal spec and can write from scratch, your approach is good when you already have the code and can create a spec post-hoc, I think. Have you followed their work?

pascal_cuoq 11y ago
I have followed the Dafny language from a distance since the beginning. The Ironclad project I am just discovering, but it is everything I would expect from Microsoft: a willingness to give formal methods a chance at real use and to get valuable feedback. The sad truth of from-scratch formal methods is that only Microsoft-like companies can afford to give them a try. And so far, of the Microsoft-like companies, only Microsoft is doing so. Regarding the verification of PolarSSL, you may find it useful to see what the entire report looks like concretely, even if it is for a now obsolete version of PolarSSL, so here: http://trust-in-soft.com/polarSSL_demo.pdf http://trust-in-soft.com/polarSSL_demo.pdf We have improved the methodology somewhat since that report was made, but it does give a prospective customer an idea of what they can expect for a recent branch of PolarSSL and for a usage of the library that we have agreed on before elaborating the report. TrustInSoft is going to announce the availability of this demo report this week; consider this a sneak preview.
- munin 11y ago
  Yes, these reports are nice. I've seen this kind of thing before and I've worked with frama-c and other tools personally. I think that there's some interest in from-scratch methods growing in government circles now that there are some empirical results, and that the consequences of rampant insecurity are starting to be broadly observed. We'll see if we can collectively get out in front of it though...

by munin 11y ago

pascal_cuoq 11y ago

I have followed the Dafny language from a distance since the beginning. The Ironclad project I am just discovering, but it is everything I would expect from Microsoft: a willingness to give formal methods a chance at real use and to get valuable feedback. The sad truth of from-scratch formal methods is that only Microsoft-like companies can afford to give them a try. And so far, of the Microsoft-like companies, only Microsoft is doing so. Regarding the verification of PolarSSL, you may find it useful to see what the entire report looks like concretely, even if it is for a now obsolete version of PolarSSL, so here: http://trust-in-soft.com/polarSSL_demo.pdf http://trust-in-soft.com/polarSSL_demo.pdf We have improved the methodology somewhat since that report was made, but it does give a prospective customer an idea of what they can expect for a recent branch of PolarSSL and for a usage of the library that we have agreed on before elaborating the report. TrustInSoft is going to announce the availability of this demo report this week; consider this a sneak preview.

munin 11y ago
Yes, these reports are nice. I've seen this kind of thing before and I've worked with frama-c and other tools personally. I think that there's some interest in from-scratch methods growing in government circles now that there are some empirical results, and that the consequences of rampant insecurity are starting to be broadly observed. We'll see if we can collectively get out in front of it though...