3 ms·

It's a slide deck, not a paper, but you might find this presentation from my class helpful: http://www.dwheeler.com/secure-class/presentations/Secure-Software-1

It's a slide deck, not a paper, but you might find this presentation from my class helpful: http://www.dwheeler.com/secure-class/presentations/Secure-Software-10-Formal-Methods.ppt http://www.dwheeler.com/secure-class/presentations/Secure-So... A specific example of software developed using formal methods is Tokeneer: http://www.adacore.com/sparkpro/tokeneer/ http://www.adacore.com/sparkpro/tokeneer/ There's a severe lack of publicly-worked examples. Most formal methods applications are private, which inhibits improvement and use. I'm an advocate for the creation of more "open proofs" where the tools, software being proved, and the proofs are all available as open source software. If we had more open proofs then it'd be a lot easier to understand, apply, and improve them.

retox 10y ago
I believe the capability of ada to be formally proven was one of the reasons it has seen use in defence and real-time systems.
- nickpsecurity 10y ago
  Well, there was the mandate plus the language itself was better than others at safety & programming in the large. The bigger reason, though, was that it was systematically designed to eliminate error from the syntax to memory handling to integrations. I mean, really thorough. Good description of all that in case anyone wants to cherry-pick safety features for use in a simpler language. http://www.adacore.com/knowledge/technical-papers/safe-and-secure-software-an-invitation-to-ada-2012/ http://www.adacore.com/knowledge/technical-papers/safe-and-s...
gravypod 10y ago
I'll definitely give this a look. I've been making posts every time this comes up and no one has been able to answer, or even quantify, what 'formal methods' where. The last time someone tried to sell me on them was accompanied by the pitch that "it means that your code proves itself that it's correct and that you will never have a bug ever" Naturally I laughed at that as I can see someone peddling bullshit when I see it. Do you mind if I email you about this powerpoint after giving it a look?
nickpsecurity 10y ago
Ha! I just posted your FLOSS page in same thread. I appreciate work you did on high-assurance SCM and FLOSS summaries. I've been posting them for years in security forums to try to get some adoption. People still ignoring it with the reproducible builds fad being a recent example of people missing the bigger picture [that was already fleshed out in high-assurance field with methods that work, FOSS tools, and industrial examples]. Still an uphill battle but recent results are amazing. Do check out Myreen et al's work and COGENT's filesystem paper if you haven't seen them: https://www.cl.cam.ac.uk/~mom22/ https://www.cl.cam.ac.uk/~mom22/ https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml

retox 10y ago

I believe the capability of ada to be formally proven was one of the reasons it has seen use in defence and real-time systems.

nickpsecurity 10y ago
Well, there was the mandate plus the language itself was better than others at safety & programming in the large. The bigger reason, though, was that it was systematically designed to eliminate error from the syntax to memory handling to integrations. I mean, really thorough. Good description of all that in case anyone wants to cherry-pick safety features for use in a simpler language. http://www.adacore.com/knowledge/technical-papers/safe-and-secure-software-an-invitation-to-ada-2012/ http://www.adacore.com/knowledge/technical-papers/safe-and-s...

gravypod 10y ago

I'll definitely give this a look. I've been making posts every time this comes up and no one has been able to answer, or even quantify, what 'formal methods' where. The last time someone tried to sell me on them was accompanied by the pitch that "it means that your code proves itself that it's correct and that you will never have a bug ever" Naturally I laughed at that as I can see someone peddling bullshit when I see it. Do you mind if I email you about this powerpoint after giving it a look?

nickpsecurity 10y ago

Ha! I just posted your FLOSS page in same thread. I appreciate work you did on high-assurance SCM and FLOSS summaries. I've been posting them for years in security forums to try to get some adoption. People still ignoring it with the reproducible builds fad being a recent example of people missing the bigger picture [that was already fleshed out in high-assurance field with methods that work, FOSS tools, and industrial examples]. Still an uphill battle but recent results are amazing. Do check out Myreen et al's work and COGENT's filesystem paper if you haven't seen them: https://www.cl.cam.ac.uk/~mom22/ https://www.cl.cam.ac.uk/~mom22/ https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml