6 ms·

Is a "bound-checking memory-safe C compiler" even possible in the general case without implementing a new Rust-like language?

by pedrocr 10y ago

ape4 10y ago
There's the convention where you put char stuff[0]; at the end of a struct and malloc has necessary.
david-given 10y ago
It certainly used to be in the old C89 days. I can't comment about C99 and above (because I don't know the spec well enough). I know there used to be a gcc patch which did exactly this. The way it works is that the C89 spec defines memory in terms of objects, and it's illegal to even think about a pointer that doesn't point into an object (or to the byte after). That is, it's not just illegal to dereference it, you're not even allowed to create one. So, because you know that every pointer must point at an object (or NULL), you encode the object and length of the object into the pointer. So pointers end up being a tuple of three words: object, object length, and offset. Now you have enough information to bounds check all accesses while still allowing pointer arithmetic within an object. Of course, in real life, people do all kinds of wrong things which de-facto C allows but which de-jure C doesn't, such as pointer arithmetic between objects. But the spec does allow bounds checking. (I abused this to implement a C to Perl compiler.) Incidentally, fun fact: the 286 memory segmentation system supports mostly-bounds-checked pointer accesses in hardware.
nanolith 10y ago
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. :)
nickpsecurity 10y ago
Yes, there's been many produced over time. Here's two that are in prototype form, one in LLVM, that could use extra attention from OSS community: https://www.cis.upenn.edu/acg/softbound/ https://www.cis.upenn.edu/acg/softbound/ https://github.com/santoshn/softboundcets-3.6.1 https://github.com/santoshn/softboundcets-3.6.1 http://safecode.cs.illinois.edu/ http://safecode.cs.illinois.edu/ https://github.com/jtcriswell/safecode-llvm37 https://github.com/jtcriswell/safecode-llvm37 When overhead is too high, there's also tools like CPI to at least stop code injections: http://dslab.epfl.ch/proj/cpi/ http://dslab.epfl.ch/proj/cpi/ There were also safer variants of C to make rewrites for safety easier: https://www.cs.uic.edu/pub/Main/PhDQualifyingExam/Sample4.pdf https://www.cs.uic.edu/pub/Main/PhDQualifyingExam/Sample4.pd... http://www.eg.bucknell.edu/~lwittie/research/Clay.pdf http://www.eg.bucknell.edu/~lwittie/research/Clay.pdf Note: Clay was used in device drivers and garbage collectors in partnership with Microsoft Research. Some Cyclone techniques were adopted in Rust. So, the tooling has been around in different forms for a long time. OpenBSD presentation even mentioned a few. They avoid safer languages and these tools on purpose in favor of C, a review process aiming to find all vulnerabilities before hackers, and their after-the-attack mitigations for when they don't. Improving something like Softbound with checks disabled on known-good modules for performance gain would be so much better in terms of time invested and benefits gained. Plus, even average app developers could make memory safe code with same tool. Not going to happen, though. It's not how mainstream "security" works. They default on using worst tools for the job for what seems to be political/social reasons more than anything. CompSci and private sector innovations long knocked out the technical ones. There's at least niche projects like Redox, GenodeOS, and Muen applying different aspects of best, known methods.

Is a "bound-checking memory-safe C compiler" even possible in the general case without implementing a new Rust-like language?

by pedrocr 10y ago

Is a "bound-checking memory-safe C compiler" even possible in the general case without implementing a new Rust-like language?

ape4 10y ago

There's the convention where you put char stuff[0]; at the end of a struct and malloc has necessary.

david-given 10y ago

It certainly used to be in the old C89 days. I can't comment about C99 and above (because I don't know the spec well enough). I know there used to be a gcc patch which did exactly this. The way it works is that the C89 spec defines memory in terms of objects, and it's illegal to even think about a pointer that doesn't point into an object (or to the byte after). That is, it's not just illegal to dereference it, you're not even allowed to create one. So, because you know that every pointer must point at an object (or NULL), you encode the object and length of the object into the pointer. So pointers end up being a tuple of three words: object, object length, and offset. Now you have enough information to bounds check all accesses while still allowing pointer arithmetic within an object. Of course, in real life, people do all kinds of wrong things which de-facto C allows but which de-jure C doesn't, such as pointer arithmetic between objects. But the spec does allow bounds checking. (I abused this to implement a C to Perl compiler.) Incidentally, fun fact: the 286 memory segmentation system supports mostly-bounds-checked pointer accesses in hardware.

nanolith 10y ago

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

nickpsecurity 10y ago

Yes, there's been many produced over time. Here's two that are in prototype form, one in LLVM, that could use extra attention from OSS community: https://www.cis.upenn.edu/acg/softbound/ https://www.cis.upenn.edu/acg/softbound/ https://github.com/santoshn/softboundcets-3.6.1 https://github.com/santoshn/softboundcets-3.6.1 http://safecode.cs.illinois.edu/ http://safecode.cs.illinois.edu/ https://github.com/jtcriswell/safecode-llvm37 https://github.com/jtcriswell/safecode-llvm37 When overhead is too high, there's also tools like CPI to at least stop code injections: http://dslab.epfl.ch/proj/cpi/ http://dslab.epfl.ch/proj/cpi/ There were also safer variants of C to make rewrites for safety easier: https://www.cs.uic.edu/pub/Main/PhDQualifyingExam/Sample4.pdf https://www.cs.uic.edu/pub/Main/PhDQualifyingExam/Sample4.pd... http://www.eg.bucknell.edu/~lwittie/research/Clay.pdf http://www.eg.bucknell.edu/~lwittie/research/Clay.pdf Note: Clay was used in device drivers and garbage collectors in partnership with Microsoft Research. Some Cyclone techniques were adopted in Rust. So, the tooling has been around in different forms for a long time. OpenBSD presentation even mentioned a few. They avoid safer languages and these tools on purpose in favor of C, a review process aiming to find all vulnerabilities before hackers, and their after-the-attack mitigations for when they don't. Improving something like Softbound with checks disabled on known-good modules for performance gain would be so much better in terms of time invested and benefits gained. Plus, even average app developers could make memory safe code with same tool. Not going to happen, though. It's not how mainstream "security" works. They default on using worst tools for the job for what seems to be political/social reasons more than anything. CompSci and private sector innovations long knocked out the technical ones. There's at least niche projects like Redox, GenodeOS, and Muen applying different aspects of best, known methods.