5 ms·

I would be interested in your repository of resources, is it something you plan to make public soon? Something I find very useful as a developer is to see how

I would be interested in your repository of resources, is it something you plan to make public soon? Something I find very useful as a developer is to see how tools work on concrete examples. For formal verification, this is well examplified by the document "ACSL by Example" about Frama-C: https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf https://github.com/fraunhoferfokus/acsl-by-example/blob/mast... This has inspired other researchers to do the same for SPARK, but currently they have done only the code/proofs, not yet the doc around it: https://github.com/yoogx/spark_examples/tree/master/spark-by-example https://github.com/yoogx/spark_examples/tree/master/spark-by... As I like that approach a lot, that's something I have adopted for the static analysis tools we develop around Ada and SPARK: http://docs.adacore.com/codepeer-docs/users_guide/_build/html/codepeer_by_example.html http://docs.adacore.com/codepeer-docs/users_guide/_build/htm... https://docs.adacore.com/spark2014-docs/html/ug/en/source/gnatprove_by_example.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/gn... This shares with the O'Reilly Cookbook series (https://ssearch.oreilly.com/?q=cookbook https://ssearch.oreilly.com/?q=cookbook) the goals to get very concrete immediately, on code that the reader might have to write or have already written.

nickpsecurity 9y ago
It's funny you mention that because I've been collecting those Frama-C, SPARK, and WhyML papers in case anyone wants to port examples between languages. One of the things I [re-]downloaded a week or two ago for that was ACSL by Example. :) I also got floating point verification (I know you all are doing that), one on string functions, and one on GMP for big integers. I don't have any of it published in an online repo yet. I mostly just submit it to Lobste.rs for their crowd that likes deeper tech and give it to individual people via social media or email. https://lobste.rs/newest/nickpsecurity https://lobste.rs/newest/nickpsecurity The stories section of that link has examples including recent ones on floating point and interior point. The interior point paper you might find interesting since they have a specific specification and coding style to achieve full automation. https://hal.archives-ouvertes.fr/hal-01681134/document https://hal.archives-ouvertes.fr/hal-01681134/document You might also find Lea Wittie's work on Clay interesting. I was looking at her dissertation in case one could use SPARK in similar way to model I/O or concurrency. https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf re your concrete examples I like that you're all doing that. That does help a lot. I plan to do my part to some degree in the near-ish future: I bought the High-Integrity Applications book for SPARK and Stavely's Toward Zero-Defect Programming for Cleanroom. http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html SPARK book looks well-written but kind of packed with info esp on the language. Might take some time for me to learn. The Cleanroom book is highly approachable with the method mostly being algebraic focused on human understanding with symbolic-style verification of some control flow mechanisms. That was from a skim, though, with full method maybe being harder. My plan is to get back into feel of doing this stuff by trying Cleanroom first followed by using what SPARK book teaches me on all the same stuff. Both during and after learning SPARK, I'll use it on little functions like in the ACSL by Example book. Note that this assumes some other research doesn't take higher priority for me like my Brute-Force Assurance concept that mixes languages with their verification tooling. I took the first steps of trying to get the SPARK GPL environment downloaded and installed. That wasn't working for some reason. It's harder than necessary to install: should be a well-packed installer like most things are on major Linux distros (esp Ubuntu) if wanting maximum adoption/experimentation. Since newest stuff from download link failed, I pulled older stuff through Synaptic which at least got GNAT working on doublec's Hello World example below. SPARK 2014 refused to run on it, though. https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spark-gpl-editions.html https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spa... So, I gotta get SPARK working on my machine before trying to learn it. Sucks that it's been this difficult. I'll try again later this week.
- yannickmoy 9y ago
  Thanks for the links to interesting articles. Definitely interested in the interior point formalization and proof. As I expected, it's already quite hard even without taking floats into account. (In the conclusion they say "We worked with real variables to concentrate on runtime errors, termination and functionality and left floating points errors for a future work.") Our experience with industrial users using floats is that most are not interested if we don't deal with floats. Otherwise no guarantees can be given for the actual code. Re learning SPARK, we'll have a brand new learning website during the year for Ada and SPARK, to replace the e-learning website u.adacore.com. This should make it far easier to learn Ada/SPARK, hopefully with online tweakable examples as on https://cloudchecker.r53.adacore.com/ https://cloudchecker.r53.adacore.com/ With the SPARK Discovery GPL 2017 edition (from https://www.adacore.com/download https://www.adacore.com/download), note that you'll get only Alt-Ergo installed by default. You need to follow these other instructions to add CVC4/Z3: http://docs.adacore.com/spark2014-docs/html/ug/en/appendix/alternative_provers.html#installing-cvc4-and-z3-for-spark-discovery http://docs.adacore.com/spark2014-docs/html/ug/en/appendix/a... If you have any problems, let's discuss on spark2014-discuss@lists.adacore.com, or report it on spark@adacore.com I'm curious about your Brute-Force Assurance concept, can you say more?
  - nickpsecurity 9y ago
    "Our experience with industrial users using floats is that most are not interested if we don't deal with floats. Otherwise no guarantees can be given for the actual code." That makes sense. The reason I kept it was that I saw some conference... https://complexity.kaist.edu/CCA2017/workshop.html https://complexity.kaist.edu/CCA2017/workshop.html ...talking about doing ERA as what looks like a replacement for floats. If it gets built, then the code for reals will either be verified directly or an equivalence checker between a real and float implementation will be next move. So, any papers verifying reals might have work that comes in handy later is my thinking. "we'll have a brand new learning website during the year for Ada and SPARK, to replace the e-learning website u.adacore.com. This should make it far easier to learn Ada/SPARK" Thank you! That and the list will probably be very helpful. "I'm curious about your Brute-Force Assurance concept, can you say more?" I was describing it a lot but I noticed a lot of verification tech is getting patented in U.S. for questionable reasons. I'm a bit concerned about possibility a party in U.S. will patent it, lock it up, or troll implementers if I describe it in detail in way that doesn't count as prior art. From what I've been told, putting it in a peer-reviewed journal would establish prior art to block that. Decent shot anyway. So, I think I'm going to try to do a detailed write-up first to make sure as many people can adopt it as possible. I'm also thinking about an appendix that consist of a brainstorming session of every way I can think of possibly applying it to block some mix-and-match type of bogus patents. I can tell you the concept involves translating a program into an equivalent representation in multiple languages to run their associated tooling on it. The results are assessed manually or automatically to see if they apply to original form. Original is fixed repeatedly until the tools each say Ok. Each tool is picked for being good at something others aren't. Rust for temporal safety, SPARK for automated proving, a tool-specific language for termination checking, (more properties/tools here), and finally C for its tooling and final release. I've seen people attempt to integrate different logics or use multiple tools. I've never seen people do that cross-language using everything from test generators to static analysis to proofs. It seems my hackish idea is pretty original. Note: Original inspiration was two fold. C had the best speed along with most tools. Most concurrency-analysis tools were for Java. I thought I could get safe concurrency in C for free by working within a C-based mockup of the Java model that Java's tools analyzed. Additionally, a lot of system code was done in C++ which is seemingly impossible to analyze as much as C. My concept was a C++-to-C compiler, apply all static analysis available in C, figure out what problems apply to C++ code, fix them, and repeat. Thinking on these for more languages and problems as I watched high-assurance certifications take years led to my hackish idea that's intended to replace rare experts with a pile of cheap, well-trained amateurs letting tools do most of the work. re verification and WhyML Whatever work I do, whether proprietary or FOSS, will be targeted in tech and price at maximizing uptake more than profit. Might be dual-licensed with intent SPARK, Frama-C, and Rust folks benefit whether building commercial stuff on it or FOSS. I noticed most build on Why3 with it having its own programming language (WhyML). I've also seen researchers working directly in WhyML to prove properties. It seems my tool should target it so both SPARK and C can use results. The correctness of assembly is still a problem with existing verified compilers being for CompCert C, C0, Simpl/C, and SML. My next cheat of an idea is compiling WhyML programs directly to assembly. So, I ask: (a) Do you think that's possible to begin with? I've only glanced at WhyML. Since I don't use it, I don't know if it's enough of a programming language that it could be efficiently compiled or too abstract for that. (b) If that's possible, then have you seen any research already trying to build a WhyML-to-assembly compiler or equivalence checker? I also always mentally retarget every assurance method I know on a new stack since high-assurance security demands we use every approach. So, when looking at this, I'm also thinking of contract-based test generation for properties expressed in Why3 on WhyML code, fuzzing the WhyML-to-x86 result with Why3 properties in as runtime checks, retargeting a static analyzer to work on it directly, and so on. If it can be verified and executed, then maybe someone can port lightweight, verification tools straight to Why3/WhyML to knock out issues before proofs or just more easily check code that would otherwise require manual proof.

nickpsecurity 9y ago

It's funny you mention that because I've been collecting those Frama-C, SPARK, and WhyML papers in case anyone wants to port examples between languages. One of the things I [re-]downloaded a week or two ago for that was ACSL by Example. :) I also got floating point verification (I know you all are doing that), one on string functions, and one on GMP for big integers. I don't have any of it published in an online repo yet. I mostly just submit it to Lobste.rs for their crowd that likes deeper tech and give it to individual people via social media or email. https://lobste.rs/newest/nickpsecurity https://lobste.rs/newest/nickpsecurity The stories section of that link has examples including recent ones on floating point and interior point. The interior point paper you might find interesting since they have a specific specification and coding style to achieve full automation. https://hal.archives-ouvertes.fr/hal-01681134/document https://hal.archives-ouvertes.fr/hal-01681134/document You might also find Lea Wittie's work on Clay interesting. I was looking at her dissertation in case one could use SPARK in similar way to model I/O or concurrency. https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf re your concrete examples I like that you're all doing that. That does help a lot. I plan to do my part to some degree in the near-ish future: I bought the High-Integrity Applications book for SPARK and Stavely's Toward Zero-Defect Programming for Cleanroom. http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html SPARK book looks well-written but kind of packed with info esp on the language. Might take some time for me to learn. The Cleanroom book is highly approachable with the method mostly being algebraic focused on human understanding with symbolic-style verification of some control flow mechanisms. That was from a skim, though, with full method maybe being harder. My plan is to get back into feel of doing this stuff by trying Cleanroom first followed by using what SPARK book teaches me on all the same stuff. Both during and after learning SPARK, I'll use it on little functions like in the ACSL by Example book. Note that this assumes some other research doesn't take higher priority for me like my Brute-Force Assurance concept that mixes languages with their verification tooling. I took the first steps of trying to get the SPARK GPL environment downloaded and installed. That wasn't working for some reason. It's harder than necessary to install: should be a well-packed installer like most things are on major Linux distros (esp Ubuntu) if wanting maximum adoption/experimentation. Since newest stuff from download link failed, I pulled older stuff through Synaptic which at least got GNAT working on doublec's Hello World example below. SPARK 2014 refused to run on it, though. https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spark-gpl-editions.html https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spa... So, I gotta get SPARK working on my machine before trying to learn it. Sucks that it's been this difficult. I'll try again later this week.

yannickmoy 9y ago
Thanks for the links to interesting articles. Definitely interested in the interior point formalization and proof. As I expected, it's already quite hard even without taking floats into account. (In the conclusion they say "We worked with real variables to concentrate on runtime errors, termination and functionality and left floating points errors for a future work.") Our experience with industrial users using floats is that most are not interested if we don't deal with floats. Otherwise no guarantees can be given for the actual code. Re learning SPARK, we'll have a brand new learning website during the year for Ada and SPARK, to replace the e-learning website u.adacore.com. This should make it far easier to learn Ada/SPARK, hopefully with online tweakable examples as on https://cloudchecker.r53.adacore.com/ https://cloudchecker.r53.adacore.com/ With the SPARK Discovery GPL 2017 edition (from https://www.adacore.com/download https://www.adacore.com/download), note that you'll get only Alt-Ergo installed by default. You need to follow these other instructions to add CVC4/Z3: http://docs.adacore.com/spark2014-docs/html/ug/en/appendix/alternative_provers.html#installing-cvc4-and-z3-for-spark-discovery http://docs.adacore.com/spark2014-docs/html/ug/en/appendix/a... If you have any problems, let's discuss on spark2014-discuss@lists.adacore.com, or report it on spark@adacore.com I'm curious about your Brute-Force Assurance concept, can you say more?
- nickpsecurity 9y ago
  "Our experience with industrial users using floats is that most are not interested if we don't deal with floats. Otherwise no guarantees can be given for the actual code." That makes sense. The reason I kept it was that I saw some conference... https://complexity.kaist.edu/CCA2017/workshop.html https://complexity.kaist.edu/CCA2017/workshop.html ...talking about doing ERA as what looks like a replacement for floats. If it gets built, then the code for reals will either be verified directly or an equivalence checker between a real and float implementation will be next move. So, any papers verifying reals might have work that comes in handy later is my thinking. "we'll have a brand new learning website during the year for Ada and SPARK, to replace the e-learning website u.adacore.com. This should make it far easier to learn Ada/SPARK" Thank you! That and the list will probably be very helpful. "I'm curious about your Brute-Force Assurance concept, can you say more?" I was describing it a lot but I noticed a lot of verification tech is getting patented in U.S. for questionable reasons. I'm a bit concerned about possibility a party in U.S. will patent it, lock it up, or troll implementers if I describe it in detail in way that doesn't count as prior art. From what I've been told, putting it in a peer-reviewed journal would establish prior art to block that. Decent shot anyway. So, I think I'm going to try to do a detailed write-up first to make sure as many people can adopt it as possible. I'm also thinking about an appendix that consist of a brainstorming session of every way I can think of possibly applying it to block some mix-and-match type of bogus patents. I can tell you the concept involves translating a program into an equivalent representation in multiple languages to run their associated tooling on it. The results are assessed manually or automatically to see if they apply to original form. Original is fixed repeatedly until the tools each say Ok. Each tool is picked for being good at something others aren't. Rust for temporal safety, SPARK for automated proving, a tool-specific language for termination checking, (more properties/tools here), and finally C for its tooling and final release. I've seen people attempt to integrate different logics or use multiple tools. I've never seen people do that cross-language using everything from test generators to static analysis to proofs. It seems my hackish idea is pretty original. Note: Original inspiration was two fold. C had the best speed along with most tools. Most concurrency-analysis tools were for Java. I thought I could get safe concurrency in C for free by working within a C-based mockup of the Java model that Java's tools analyzed. Additionally, a lot of system code was done in C++ which is seemingly impossible to analyze as much as C. My concept was a C++-to-C compiler, apply all static analysis available in C, figure out what problems apply to C++ code, fix them, and repeat. Thinking on these for more languages and problems as I watched high-assurance certifications take years led to my hackish idea that's intended to replace rare experts with a pile of cheap, well-trained amateurs letting tools do most of the work. re verification and WhyML Whatever work I do, whether proprietary or FOSS, will be targeted in tech and price at maximizing uptake more than profit. Might be dual-licensed with intent SPARK, Frama-C, and Rust folks benefit whether building commercial stuff on it or FOSS. I noticed most build on Why3 with it having its own programming language (WhyML). I've also seen researchers working directly in WhyML to prove properties. It seems my tool should target it so both SPARK and C can use results. The correctness of assembly is still a problem with existing verified compilers being for CompCert C, C0, Simpl/C, and SML. My next cheat of an idea is compiling WhyML programs directly to assembly. So, I ask: (a) Do you think that's possible to begin with? I've only glanced at WhyML. Since I don't use it, I don't know if it's enough of a programming language that it could be efficiently compiled or too abstract for that. (b) If that's possible, then have you seen any research already trying to build a WhyML-to-assembly compiler or equivalence checker? I also always mentally retarget every assurance method I know on a new stack since high-assurance security demands we use every approach. So, when looking at this, I'm also thinking of contract-based test generation for properties expressed in Why3 on WhyML code, fuzzing the WhyML-to-x86 result with Why3 properties in as runtime checks, retargeting a static analyzer to work on it directly, and so on. If it can be verified and executed, then maybe someone can port lightweight, verification tools straight to Why3/WhyML to knock out issues before proofs or just more easily check code that would otherwise require manual proof.