OpenBSD 6.0 released

"Also true for many embedded apps given the remaining runtime hit can range from single-digits to 40% depending on scheme used."

I think that depends on the definition of embedded. When one is lucky enough to work with a chipset in which a 40% performance hit still results in acceptable performance, such a tool is reasonable. I can tell you from my experience in the consumer electronics field that BOM costs often rule over software performance, and as such, firmware engineers are often stuck with finding creative ways to solve problems on nerfed hardware. Wrestling with a tool that can occasionally inject unwanted runtime overhead in unpredictable locations can compound razor-thin time-to-market timelines for last minute BOM changes.

The focus for my tool is to provide people with the ability to build additional propositions that go beyond basic correctness or memory bounding found in tools like Astree. Astree, for instance, may be able to automatically discover whether a subset of C is correct -- because it has a very reasonable policy of assuming incorrect behavior unless otherwise proven -- but it can't solve for custom policies such as, "does this seemingly correct code actually follow my architecture and specification?"

Also, Astree isn't free software. It's an AbsInt product, which means most likely that it comes with a hefty price tag. To give you an idea, their CompCert compiler is licensed in the five to six figure Euro range per seat. Of course, for the sort of customers AbsInt is interested in -- companies like Airbus or Boeing -- this isn't necessarily a deal breaker. They are willing to pay for such a tool because of the mission critical aspect of their work.

But, I'm of the opinion that the industry as a whole needs access to tools like these. The tool I'm building will be released under the LGPL. The security problem is one with which the entire industry needs to engage. My tool may not necessarily be the best one out there -- nor am I trying to build the best tool -- but I am trying to build one that is "good enough" and reasonably sound. I think I have struck the right balance, but time will tell.

I wouldn't say that I'm a formal methodist as much as a software engineer looking to be able to make strong guarantees about critical components. I have a problem to solve, and I've spent a few years studying this problem off and on. Somewhere along the way, I acquired enough hubris, if not enough knowledge, to think that I could build such a tool. So far, things have worked out better than I've thought. But, I still have a few big hurdles to overcome before I can confidently say that this tool will be useful to others. INRIA and other researchers have blazed the trail, and they have rightfully charged a small fortune for what they have discovered. I'm much more interested in ensuring that the average developer has access to such technology. My tool won't have the bells and whistles of commercial offerings, but it's hard to beat the price.

Alright, this sub-thread started with a person wondering if one could make C programs memory-safe against common errors. You replied with formal verification while I replied with automated tools that make C memory safe. One or two use formally-verified models. :) You countered with the needs of embedded making such tools impractical. There's many in that industry that can use tooling like I recommended, esp if not BOM-sensitive or hard real-time. You brought up the needs of ultra-constrained market in terms of cost or hard real-time. The increasing market-share of expensive ARM's vs 8-16-bitters and embedded JVM's makes me wonder if that's oversimplified, too. Makes me think similar companies might consider tooling like I described if it likewise adds benefit with tiny costs. The majority will do as you say and avoid these tools since they don't fit their use case. So will some non-embedded sectors focused only on performance or lowest cost.

Let's cut to some important stuff, though, as I think the argument got over semantics or at least less interesting stuff. My background is high-assurance security with generalist experience but none with formal methods or building static analyzers. You seem to have experience in those I don't. Appel, who makes the tool you linked, is a formal methodist (among other things) building stuff that's useful, achieves high-end stuff, and sometimes enabling less-skilled people. Rare type of researcher and deliverables I love seeing. You say you want to do something similar. So, let's have a more interesting conversation.

"Also, Astree isn't free software. It's an AbsInt product" (and CompCert)

I saw writing on wall with CompCert when they hesitated to FOSS it or answer questions. So sad such a wonderful tool got locked up. Thanks for confirming with a dollar range what I suspected. Same with Astree. We need replacements for both like you said about CompCert. My first idea was for a team to clone CompCert based on high-level description of what it does with dependent types a la Chlipala or just FLINT ML-style compiler. Add Design-by-Contract, QuickCheck, and a few other things with take little time but collectively knock out tons of errors. Compile it with MLton for development speed and CakeML for release version with equivalence checks. Be 90+% to quality of formal verification without CompCert and have a nice foundation for whoever wants to go fully formal.

Far as what formal people were doing, first I saw were trying to use a micropass approach to piecemeal build one for a MIPS machine where they spent tiny fraction of time of CompCert. Don't have link handy or know their status. Fortunately, Myreen et al's method already got used in seL4. A lot more than that actually haha. Perhaps a short-cut to CompCert replacement is to automate the process of running a C subset through such tooling with possibly guidelines for programmers a la MISRA to keep automated part feasible? Existing tools, esp AutoCorres/Simpl, should have solved hardest problems in that.

"But, I'm of the opinion that the industry as a whole needs access to tools like these." "The security problem is one with which the entire industry needs to engage"

You preaching to the choir. I was designing and preaching high-assurance security, at least for critical stuff (eg kernels, compilers), way before the Snowden leaks. The stuff mainstream, "INFOSEC professionals" said was hypothetical in risk or overkill in solution was often validated by specific attacks in leaks. ;) Odd thing is they still argue with us and dismiss high-assurance as red tape or 100% impractical. Same with things like SPARK. (rolls eyes) Anyway, I published for free a summary of high-security INFOSEC on Schneier's blog in 2013 in an argument about secure code != secure systems:

http://pastebin.com/y3PufJ0V

"but I am trying to build one that is "good enough" and reasonably sound. I think I have struck the right balance, but time will tell."

I encourage people to do exactly what you're doing. There will be no one-size-fits-all. Tools that approach these analyses balancing ease-of-use with properties proven or bugs found are best bet because it's all time-constrained developers will likely use. I'm also glad you're FOSSing it. I don't expect a community to show up as FOSS types ignore most high-security stuff. The model I'm pushing for is businesses licensing software or selling hardware leveraging high-assurance components with a percentage of revenue put into improving or maintaining them. On top of what practical, grant-funded academics contribute. FOSS is still a pre-requisite to this model working as likes of AbsInt or Alt Software keep barrier-to-entry too high with licensing costs. Medium-to-high assurance might cost money and time to develop but access to it has to be cheap and easy for uptake. Ironies of life.

"I wouldn't say that I'm a formal methodist." " Somewhere along the way, I acquired enough hubris, if not enough knowledge, to think that I could build such a tool."

Lol. That's how it starts. You'll be asking me to trust 100 pages of proof because the checker said so within 3-5 years. :P

Seriously, though, I'm glad you're not cocky as being careful & using many methods for correctness is best route. At least one always misses something. Even happened to CompCert where the spec was wrong 2-3 times but at least the code faithfully implemented the bad spec. You might dodge that if more careful & testing every part of lifecycle.

" My tool won't have the bells and whistles of commercial offerings, but it's hard to beat the price."

Good luck to you on that. While we're at it, the last time I heard something like this was someone telling me about Liquid Types analyzer for C programs (below). What do you think of it for this problem area or versus your own approach? Or if someone like me with no specialist skill should attempt to mess with it? Very hard for me to evaluate that aspect. I fear I will waste dozens to hundreds of hours on the wrong approach haha.

http://goto.ucsd.edu/csolve/

I agree with your synopsis on Pastebin. It's pretty close to what I have been trying to practice. As an interesting aside, I worked with a few researchers about a decade ago on tracking SMM vulnerabilities in various Intel chipsets. They were the experts though. I was just a hired hand. Still, I learned a lot about the very real threat of hardware vulnerabilities.

The Liquid Types approach used in CSolve -- if memory serves correctly -- makes use of an SMT solver to attempt to find counter-examples given a particular set of constraints. This is similar to the approach that Frama-C uses. SMT solvers are interesting and can do quite a bit, but they are still incomplete. Many linters have started incorporating SMT solvers. It's better than much of what is out there, but there are still significant limitations. Furthermore, the markup languages provided are often limited in the amount of customization that can be performed.

My tool is designed as a framework that can be used to build much more comprehensive proofs. Similar to what you posted in Pastebin, the security of a system is intimately tied to the architecture of a system as a whole. I want to formally verify the architecture, then demonstrate that the implementation is operating under the constraints of the architecture using a combination of equivalency and bounding proofs. This, in conjunction with a strong understanding and integration with the sorts of runtime features available in a system (i.e. MMU protections) can be used to build a compelling verified proof of security similar to what was done with seL4.

But, ultimately, even this is not enough. Few systems today are contained within a single machine. IoT has demonstrated just how complex the current software ecosystem is becoming. Security proofs must extend beyond individual applications and systems and cover heterogenous and widely distributed systems with many different potential attack vectors. This can be formally verified, but as far as I'm concerned, such a verification is an architecture-first approach. I don't think that in this sort of environment, a correctness tool is enough. It's a great addition to the toolbox, and it is a damned useful tool at that, but correct software can still violate policy unless this policy is part of the constraint of "correct".

I'm mixed about the post, esp the science part. The science of developing robust software is great and pretty consistent going back decades varying mostly in specific tools and tactics. Mainstream programming just doesn't apply it although more adoption in past decade of key techniques. Here's some computer science from the 1960's-1980's used in robust and secure system development (esp Orange Book B3 or CC EAL6) people might want to copy. I'm taking an empirical route where I reference techniques that were applied to many real-world projects with lessons learned in papers or studies that were consistent. All one can do with limited data & these aren't in order of importance.

1. Formal, non-English (eg math/logical) specifications of requirements or abstract design. English is ambiguous and misreadings of it caused countless errors, even back then. CompSci researchers tried formal specs with both English as a start and precise notations (eg Z, VDM, ASM's, statecharts) for clarity in specifics. Result was many inconsistencies caught in highly assured systems and protocol specs before coding even began.

2. High assurance stuff often used mathematical (formal) verification. Whether that worked or made sense was hit and miss. More on it later. Yet, virtually all of them said there was benefit in restrictions on the specs, design, and coding style to fit the provers' limitations. Essentially, they used boring constructs that were easy to analyse and this prevented/caught problems. Don't be too clever with design or code. Wirth and Hansen applied this to language design to bake safety & comprehension in with minimal to low loss in performance.

Note: Led to Nick P's Law of Trustworthy Systems: "Tried and true beats novel or new." Always the default.

3. Dijkstra's THE project showed that modular, layered design with careful attention to interfaces (and interface checks) makes for most robust and maintainable software. Later results confirmed this where each module must fit in your head and control graph that's pretty predictable with minimal cycles prevented all kinds of local-becomes-global issues. Many systems flawless (or nearly so) in production were built this way. Dijkstra correctly noted that it was very hard to do this even for smart people and average developer might screw structuring up a lot. Solid prediction... but still worth striving for improvement here.

4. Fagan ran empirical studies at IBM that showed a regular, systematic, code review process caught many problems, even what tests missed. Turned that into formal inspections with the periodicity and prioritizing tuned per organization for right cost-benefit. Was generalized to whole SDLC by others in high robustness areas. Improved every project that used it from then on. Exactly what parameters to use is still open-ended but periodically looking for well-known flaws with reference sheet always works.

5. Testing for every feature, code-path, prior issues outside of code base, and common use-case. All of these have shown repeated benefits. There's a cut-off point for each that's still an open, research problem. However, at a minimum, usage-based testing and regression testing helped many projects achieve either zero or near-zero, user-facing defects in production. That's a very important differentiator as 100 bugs user never experiences is better than 5 that they do regularly. Mills' Cleanroom process combined simple implementation, code review, and usage-testing for insanely-high, statistically-certifiable quality even for amateur teams.

6. By around 60's-70's, it became clear that the language you choose has a significant effect on productivity, defects, maintenance, and integration. Numerous studies were run in industry and military comparing various ones. Certain languages (eg Ada) showed vastly lower defects, equal/better productivity, and great maintenance/integration in every study. Haven't seen many such studies since the 90's and most aren't constructed well to eliminate bias. However, it's grounded in science to claim that certain language choices prevent common negatives and encourage positives. So, it follows to adopt languages that make robust development easier.

7. By the 80's or 90's, it was clear that computers were better at finding certain problems in specs and code than humans. This gave rise to methodologies that put models of system or code into model-checkers and provers to show certain properties always hold (the good) or never show up (the bad). Used successfully with high-assurance safety and security critical systems with results ranging from "somewhat beneficial" to "caught stuff we'd never see or test for." Back then it was unclear how applicable it was. Recent work by Chlipala, Leroy, et al show near perfect results in practice when specs/proofs are right and much wider application than before. Lots of tooling and prior examples means this is a proven way of getting extra quality where high-stakes are worth the cost and where core functionality doesn't change often.. The CompCert C compiler, Eiffel's SCOOP concurrency scheme, and Navy team's EAL7 IPsec VPN are good examples.

8. Static analysis, aka "lightweight formal methods," were devised to deal with specialized skills and labor of above. Getting to the point, tools like Astree Analyzer or SPARK Ada can prove absence of common flaws with little to no false positives without need for mathematicians in the company. Just a half dozen of these tools by themselves found tons of vulnerabilities in real-world software that passed human review and testing. Enough said, eh?

9. Software that succeeded with testing often failed when random stuff came at it, especially malware. This led to various fault-injection methods like fuzz testing to simulate that and find breaking points. The huge number of defects, esp in file formats & protocol engines, found via this method argues for its effectiveness in improving quality. It ties in with stuff above in that well-written code that validates input at interface and preserves invariants throughout execution should simply disregard (or report) such erroneous input.

10. Interface errors themselves posed something like 80+% of problems. This was noted as far back as the 60's in Apollo project when Margaret Hamilton invented software engineering, fault-tolerance, and specification techniques to fight it. Dijkstra and Hoare pushed for pre- and post-conditions plus specific invariants to document the assumptions of code during procedure calls. Modern version is called Design by Contract in Eiffel, Ada, and numerous other languages (even asserts in C). Many deployments and tests showed such interface checks caught many issues, esp assumption violations when new code extended or modified legacy.

11. Concurrency issues caused all kinds of problems. Techniques were devised by Hansen (Concurrent Pascal) and later Meyer et al (SCOOP) to mostly immunize against them at language level with acceptable performance. Languages without that, especially Java, later got brilliant tooling that could reliably find race conditions, deadlocks, or livelocks. Use of any method inevitably found problems in production code that had escaped detection. So, using prior, proven methods to immunize against or detect common errors in concurrency is A Good Thing. Note that shared-nothing, event-driven architectures also emerged but I have less data on them outside that some (NonStop, Erlang) worked extremely well.

The above are just a few things that computer science established with supporting evidence from real-world projects so long ago that Windows didn't exist. Anyone applying these lessons got benefits in terms of code quality, security, and maintainability. The rare few applying most or all of them, mainly high assurance community, got results along lines of space shuttle control code with extremely, low defects or zero in production. So, given the past and present results of these methods every time they're put to the test, I'm irritated every time another person talks like there's no good science to quality software. I just listed a bunch of it, it's been tested in production as scientific method requires thousands of time, tweaked probably hundreds, and core approaches remained even if tactics got modified.

Now people can feel free to use and improve on the science. CompSci continues to in every area I listed with a chunk of proprietary and FOSS developers using a subset of the techniques. Just need more uptake. Use what's proven. And do note that there's plenty of examples for specific design and implementation decisions for common types of functionality. Many things that were shown to work or not work that could be encoded in libraries, DSL's, templates, whatever. No excuse except for our field's continual failure to learn and hand down the lessons from the past.

http://pastebin.com/xZ6m4T8Z

It is upon the shoulders on these giants where I stand. Dijkstra, Floyd, Hoare, Knuth, Curry, Church, and Turing, among others.

The science exists. The trick now is bringing it all together in a way that is useful enough to others that they actually start using it. :-)