3 ms·

"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 de

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

nickpsecurity 10y ago
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 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/ http://goto.ucsd.edu/csolve/

nickpsecurity 10y ago

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 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/ http://goto.ucsd.edu/csolve/