6 ms·

Yes. But, you typically have to use a theorem prover to build up static checking for functions, and then enforce proof obligations on callers to said functions

Yes. But, you typically have to use a theorem prover to build up static checking for functions, and then enforce proof obligations on callers to said functions. If done in a system like Coq or Isabelle, the proof obligations become a parallel markup to C that is used in conjunction with the source code to enforce policies. Bounds checking is one policy -- and a relatively easy one to implement at that -- and other policies can be stacked. Take a look at VST for an example already in the wild. I'm currently working on a somewhat different approach that does not have the severe license restrictions that CompCert has. http://vst.cs.princeton.edu/download/ http://vst.cs.princeton.edu/download/

nickpsecurity 10y ago
That's not true. You just use a compiler transformation. See this: https://news.ycombinator.com/item?id=12407156 https://news.ycombinator.com/item?id=12407156 Difference between memory safety and full, formal verification of correctness. You're describing the latter. Definitely check out Myreen et al's CakeML work, COGENT at NICTA, and AutoCorres/Simpl used in seL4. They might have stuff to speed up your own tool development. I wish you great luck on your project. :)
- nanolith 10y ago
  Compiler transformation can solve most of these concerns, but it is not perfect due to undecidability. Compiler transformations will always be conservative, falling back on runtime enforcement. The main edge cases I've run into -- hence my need for building a tool like this -- is dealing with tight performance concerns found in realtime and embedded applications. Falling back to runtime enforcement is not an option, and neither is trusting developers to be able to fully analyze complex control-flow and data-flow paths without solid tooling. For general-purpose applications, of course, compiler transformation with runtime fallbacks is perfectly acceptable.
  - nickpsecurity 10y ago
    "is dealing with tight performance concerns found in realtime and embedded applications" I thought tools like Astree and SPARK have knocked this out the park. Copilot was also pretty good on runtime side given it works in embedded. Just gotta structure your program to use the tools. I think they should cover plenty of use-cases given stuff like IRONSIDES DNS runs in SPARK. "For general-purpose applications, of course, compiler transformation with runtime fallbacks is perfectly acceptable." Also true for many embedded apps given the remaining runtime hit can range from single-digits to 40% depending on scheme used. Even more combined with something like SPARK or Astree for stronger, static analysis than the minimal stuff academics usually use. Certainly a subset will benefit from or even need methods you prefer but many won't. It's just management or a consumer's preference to save a few bucks shooting them in the foot. ;) Do shoot me an email, though, in case I get some free time to run some ideas by you. I don't know enough formal methodists these days. My mile-high perspective can only let me do so much as a generalist. Gotta have specialists to help me filter the chaff from the wheat. Then pass such recommendations onto more specialists as always. :)
    - nanolith 10y ago
      "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

That's not true. You just use a compiler transformation. See this: https://news.ycombinator.com/item?id=12407156 https://news.ycombinator.com/item?id=12407156 Difference between memory safety and full, formal verification of correctness. You're describing the latter. Definitely check out Myreen et al's CakeML work, COGENT at NICTA, and AutoCorres/Simpl used in seL4. They might have stuff to speed up your own tool development. I wish you great luck on your project. :)

nanolith 10y ago
Compiler transformation can solve most of these concerns, but it is not perfect due to undecidability. Compiler transformations will always be conservative, falling back on runtime enforcement. The main edge cases I've run into -- hence my need for building a tool like this -- is dealing with tight performance concerns found in realtime and embedded applications. Falling back to runtime enforcement is not an option, and neither is trusting developers to be able to fully analyze complex control-flow and data-flow paths without solid tooling. For general-purpose applications, of course, compiler transformation with runtime fallbacks is perfectly acceptable.
- nickpsecurity 10y ago
  "is dealing with tight performance concerns found in realtime and embedded applications" I thought tools like Astree and SPARK have knocked this out the park. Copilot was also pretty good on runtime side given it works in embedded. Just gotta structure your program to use the tools. I think they should cover plenty of use-cases given stuff like IRONSIDES DNS runs in SPARK. "For general-purpose applications, of course, compiler transformation with runtime fallbacks is perfectly acceptable." Also true for many embedded apps given the remaining runtime hit can range from single-digits to 40% depending on scheme used. Even more combined with something like SPARK or Astree for stronger, static analysis than the minimal stuff academics usually use. Certainly a subset will benefit from or even need methods you prefer but many won't. It's just management or a consumer's preference to save a few bucks shooting them in the foot. ;) Do shoot me an email, though, in case I get some free time to run some ideas by you. I don't know enough formal methodists these days. My mile-high perspective can only let me do so much as a generalist. Gotta have specialists to help me filter the chaff from the wheat. Then pass such recommendations onto more specialists as always. :)
  - nanolith 10y ago
    "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.