[nickpsecurity]

"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

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

[yannickmoy]

Funny that you pointed to the workshop at KAIST. My colleague Johannes Kanig presented SPARK there, he's on the front row with a SPARK t-shirt. :-)

Regarding your Brute-Force Assurance Concept, it connects to the concept we're pushing at AdaCore of System to Software Integrity, in which we're looking at ways to preserve assurance from higher level descriptions at system level down to code. I must admit we're still in the early stages, exploring with customers how to go from SysML or Simulink to code in SPARK while preserving properties.

Your concept of using the best available tools is certainly attractive, if indeed they can be made to collaborate, and if the translations can be made trustworthy. That's something we're quite familiar with, as this is the bread-and-butter for tool building really. :-) One of the challenges in connecting languages and tools is that all the pieces are constantly moving. This is also what makes C so attractive as an intermediate language: it does not move.

WhyML has some advantages as an intermediate language. But note that the way we use it in our SPARK toolchain would not allow compiling through WhyML. Our translation only preserves the axiomatic semantics of the program, not its operational semantics. So we try to get equi-provability, but not an executable WhyML code.

If you start with WhyML though, you can either extract it to OCaml (see http://why3.lri.fr/doc-0.83/manual009.html) or to C (see https://hal.inria.fr/hal-01519732v2/document). One of the authors of this last paper, Raphael Rieu-Helft, is currently doing his PhD on getting this extraction to C formally proved, so that it can be used for efficient security components in WhyML. So maybe what you're looking at could be done with formally verified translation from WhyML to C and then formally verified compilation to assembly. We've also looked at having a SPARK frontend to CompCert in the past, but so far we've seen no commercial interest in that approach.

Thanks for your thoughts on that topic!

[nickpsecurity]

"if indeed they can be made to collaborate, and if the translations can be made trustworthy."

That is the trick. I think at the least one can, aside from using subsets close to each other, use equivalence tests that runs through all paths and key values of ranges. In high-assurance systems, one should already be using such tools given they'll catch lots of errors. So, the same tests can be re-run on the new variant in new language to see if it gives same output. This might produce reasonable, if not perfect, level of confidence. If going for semantic checks, I'm eyeballing the K Framework that was used in the C Semantics by Runtime Verification Inc. Connecting that semantics to C++, SPARK, or Rust has its own advantages. Alternatively, I work in Abstract State Machines annotated with the properties of execution that lets me then just do equivalence checks on ASM's. There's a compiler that does that.

"This is also what makes C so attractive as an intermediate language: it does not move."

That's one reason to value it. I recommend C compatibility by default these days to take advantage of ecosystem of tooling, esp compilers and verification, without performance penalties or abstraction gap failures. Although I used to recommend alternatives, the bandwagon effect showed itself to be unbeatably powerful. Some new languages getting rapid adoption are doing so partly due to seemless integration with C or otherwise legacy code. So, if I was designing SPARK-like language today, it would use C's data types and calling conventions with a compile-to-C option available from day 1. I'd possibly even build it on top of C itself with metaprogramming.

I don't like having to do such things. The momentum behind C deployment from embedded to PC to servers is just too huge. The shooting BB at freight train metaphor comes to mind. ;)

"But note that the way we use it in our SPARK toolchain would not allow compiling through WhyML."

Appreciate the tip. Means executable version of SPARK in Why might even make nice side project for some student. Thanks for the links. The Why-to-C work I submitted to Lobste.rs previously. It was great to see someone tacke GMP. I didn't know he was formally proving Why-to-C, though. If he does, your WhyML-to-C-to-assemby idea is a neat possibility. Here's one in return in case you haven't seen it that extracts Coq to C with several fold reduction in TCB. Might allow proven-C to be integrated into SPARK work or be modifiable to extract to SPARK for SPARK+Coq work.

https://staff.aist.go.jp/tanaka-akira/succinct/slide-pro114....

"We've also looked at having a SPARK frontend to CompCert in the past, but so far we've seen no commercial interest in that approach."

I have a love/hate perception of CompCert: love the work, hate it went proprietary. I imagine AbsInt charges a fortune for commercial licenses. If so, that could motivate the no commercial interest part given they'd pay two companies. Have you all thought about using one of the other toolchains that's FOSS to do that stuff? Aside from CompCert, there's these: Flint's C0 used in Verisoft; Simpl with Simpl/C used for seL4; KCC's K Framework + C Semantics; CakeML. The first three would be modified for SPARK using any SPARK-to-C mapping and/or tools you already have with some portion of work, esp on low-level stuff, already done for you. Such are most practical. I'm sure you raised an eyebrow at CakeML. My idea, which a proof engineer independently came up with, was using the imperative, low-level IR's as a target for stuff verified Why3-style or certified compilers. He was using StackLang with me looking at WordLang. Either way, the starting point is an imperative language with formal semantics verified down to machine code for x86, PPC, and ARM. Again, only sensible if C-based or more SPARK-like toolchains look impractical but these IL's do somehow.

[yannickmoy]

We have a compiler from a subset of Ada & SPARK to C: http://docs.adacore.com/live/wave/gnat_ccg/html/gnatccg_ug/g...

But that's not the same as having a full certified (in the sense of Coq) compiler. If we were to use a CompCert-like approach, we'd have to redo it in Coq. Not a small feat.

Regarding approaches that build safety/security by developing a language on top of C, that has been tried so many times that I don't think it can work. The use of the same syntax is deceptive, as you end up doing a lot of redesign/rewrite (as anyone who has done program proof would expect), so none of these sticked. Even those trying to enforce properties by design and runtime checking instead of proof (CCured, Cyclone). Better to stick with C then and use an appropriate toolset like Frama-C.