6 ms·

It's possible to program in C in a way that is memory safe and verify it programmatically (even with memory allocations and recursion). It's even do static veri

It's possible to program in C in a way that is memory safe and verify it programmatically (even with memory allocations and recursion). It's even do static verification of the absence of runtime errors, arithmetic overflows, inconsistent locking, etc. Best tools are commercial unfortunately.

pcwalton 9y ago
Can you elaborate as to how to prevent use-after-free statically in C without forbidding dynamic memory allocation?
- Nokinside 9y ago
  By proving that memory references don't live longer than the allocated memory. The use of dynamic allocation must be carefully restricted and programmer may need to provide provide assertions or modify the code to pass verification. There is two ways tho think static verification: 1. Language level verification. All valid programs are verified to be correct in respect of safety guarantees the language gives. 2. Verification of safety features that can't be proved in general. In most cases it's possible to write program in a way that it can be verified to be correct, but finding a way to write provably correct program may need some work.
  - pjmlp 9y ago
    Now try to use that in the presence of commercial libraries.
    - jhasse 9y ago
      Try to use Rust in the presence of commercial libraries.
      - pjmlp 9y ago
        Easy just like any compiler for a memory safe language. There might exist logical bugs, but the language semantics allow for a higher thrust of code quality, assuming the binaries haven't been tampered with. Every line of C code is unsafe, specially if the binary was compiled with -O3. Regarding Rust, the only issue is lack of support for binary libraries in Cargo, one needs to call rustc directly.
  - Rusky 9y ago
    Linux doesn't do any of this, and doing so is tantamount to running a borrow checker on the code, which requires more information than is present in vanilla C.
  - pcwalton 9y ago
    At that point you will have basically reinvented Rust. The resulting language will be so incompatible as to essentially be a new language.
- fpoling 9y ago
  A static checker for C code can do the similar checks that the borrow checker in Rust does. Essentially it enforces a variation of linear type system. Note that many things for Rust are on ideas from Cyclone [1], that was a research project to provide minimal extensions to C type system to ensure memory safety. [1] - https://cyclone.thelanguage.org/ https://cyclone.thelanguage.org/
  - pjmlp 9y ago
    Only works if 100% of the code is available, thus not usable by companies selling commercial libraries.
    - fpoling 9y ago
      Static checker can work in principle on binary code. Alternatively, one can annotate API the library provides for the static checker. This is especially feasible with C where API types and usage is typically rather simple. Clearly, this implies trusting API to be implemented correctly or at least using the static checker to prove that memory-safety bugs are originated in the library, not in the application code.
    - jcelerier 9y ago
      That's not really relevant when talking about the linux kernel, though, is it ? There's tons and tons of open-source code that could just run clang-analyze today and eliminate swathes of memory bugs.
      - pjmlp 9y ago
        Sure it is, starting by the GPU drivers.
  - pcwalton 9y ago
    I read the Cyclone papers when I designed the original Rust borrow checker, and we spoke to Dan Grossman. Cyclone only works because it uses garbage collection for the heap. There is a uniqueness extension, but it is limited compared to what Rust can do. (See Grossman's "Existential Types for Imperative Languages" presentation for details.) The uniqueness extension was not designed to (and is not flexible enough to) supplant the garbage collector in most real-world projects. This theoretical static checker for C code would not be compatible with virtually any existing C code in the wild, and so it would be effectively a new language.
pjmlp 9y ago
I have been hearing that since about 1990, never materializes, even on projects where Insure++ was being use. Not even Frama-C can prevent all use cases, if developers don't care.
- fpoling 9y ago
  I wonder what makes C so different from Ada where static verifies are used successfully. Is it because typical C code uses way too many pointers making full static verification much harder?
  - pjmlp 9y ago
    Language semantics, most of C errors that lead to memory corruption are simply forbidden in Ada. There is no way to corrupt memory in Ada unless you explicitly import one of the Unchecked packages and ask the compiler permission to do naughty stuff.
  - jcelerier 9y ago
    > Ada where static verifies are used successfully. and yet even ADA's standard library sometimes has bugs: http://blog.adacore.com/formal-verification-of-legacy-code http://blog.adacore.com/formal-verification-of-legacy-code
    - pjmlp 9y ago
      Sure, every programming language can have bugs. However C gets the usual set of logical errors, common to any safe programming language, memory corruption caused by lack of checks on memory access and implicit type conversions, and 200+ cases of UB when taking advantage of full compiler optimizations. Reducing the amount of possible errors per line of code is already a plus, even if doesn't remove all of them.
    - touisteur 9y ago
      Note the article you're citing is going from Ada (already strong safety checks, but you can still write bugs, just not a whole class of them) to Spark2014, so formal proof of absence of runtime errors (first) and automated verification of functional properties. Even nicer, in a stdlib, so not a toy example and something to build on... You're showing (thanks !) how to go (with some effort, but not so much) from 'so much safer than C already' to 'no bug let's move on and maybe remove all the runtime checks to get C-like performance or better'. I'd say it looks pretty cool.
adrianN 9y ago
It's probably easier to use a language that has those guarantees already than trying to bolt them onto C. Those tools and coding standards are useful if you're constrained to using C for whatever reason, e.g. if you're on an embedded platform that only has a vendor compiler. For general purpose hardware you have a lot fewer headaches if you start with a language that was designed for safety.
- margorczynski 9y ago
  And I think the compiler/interpreter can optimize the code much better when the creators know that such constructs are available in the language itself

pcwalton 9y ago

Can you elaborate as to how to prevent use-after-free statically in C without forbidding dynamic memory allocation?

Nokinside 9y ago
By proving that memory references don't live longer than the allocated memory. The use of dynamic allocation must be carefully restricted and programmer may need to provide provide assertions or modify the code to pass verification. There is two ways tho think static verification: 1. Language level verification. All valid programs are verified to be correct in respect of safety guarantees the language gives. 2. Verification of safety features that can't be proved in general. In most cases it's possible to write program in a way that it can be verified to be correct, but finding a way to write provably correct program may need some work.
- pjmlp 9y ago
  Now try to use that in the presence of commercial libraries.
  - jhasse 9y ago
    Try to use Rust in the presence of commercial libraries.
    - pjmlp 9y ago
      Easy just like any compiler for a memory safe language. There might exist logical bugs, but the language semantics allow for a higher thrust of code quality, assuming the binaries haven't been tampered with. Every line of C code is unsafe, specially if the binary was compiled with -O3. Regarding Rust, the only issue is lack of support for binary libraries in Cargo, one needs to call rustc directly.
- Rusky 9y ago
  Linux doesn't do any of this, and doing so is tantamount to running a borrow checker on the code, which requires more information than is present in vanilla C.
- pcwalton 9y ago
  At that point you will have basically reinvented Rust. The resulting language will be so incompatible as to essentially be a new language.
fpoling 9y ago
A static checker for C code can do the similar checks that the borrow checker in Rust does. Essentially it enforces a variation of linear type system. Note that many things for Rust are on ideas from Cyclone [1], that was a research project to provide minimal extensions to C type system to ensure memory safety. [1] - https://cyclone.thelanguage.org/ https://cyclone.thelanguage.org/
- pjmlp 9y ago
  Only works if 100% of the code is available, thus not usable by companies selling commercial libraries.
  - fpoling 9y ago
    Static checker can work in principle on binary code. Alternatively, one can annotate API the library provides for the static checker. This is especially feasible with C where API types and usage is typically rather simple. Clearly, this implies trusting API to be implemented correctly or at least using the static checker to prove that memory-safety bugs are originated in the library, not in the application code.
  - jcelerier 9y ago
    That's not really relevant when talking about the linux kernel, though, is it ? There's tons and tons of open-source code that could just run clang-analyze today and eliminate swathes of memory bugs.
    - pjmlp 9y ago
      Sure it is, starting by the GPU drivers.
- pcwalton 9y ago
  I read the Cyclone papers when I designed the original Rust borrow checker, and we spoke to Dan Grossman. Cyclone only works because it uses garbage collection for the heap. There is a uniqueness extension, but it is limited compared to what Rust can do. (See Grossman's "Existential Types for Imperative Languages" presentation for details.) The uniqueness extension was not designed to (and is not flexible enough to) supplant the garbage collector in most real-world projects. This theoretical static checker for C code would not be compatible with virtually any existing C code in the wild, and so it would be effectively a new language.

pjmlp 9y ago

I have been hearing that since about 1990, never materializes, even on projects where Insure++ was being use. Not even Frama-C can prevent all use cases, if developers don't care.

fpoling 9y ago
I wonder what makes C so different from Ada where static verifies are used successfully. Is it because typical C code uses way too many pointers making full static verification much harder?
- pjmlp 9y ago
  Language semantics, most of C errors that lead to memory corruption are simply forbidden in Ada. There is no way to corrupt memory in Ada unless you explicitly import one of the Unchecked packages and ask the compiler permission to do naughty stuff.
- jcelerier 9y ago
  > Ada where static verifies are used successfully. and yet even ADA's standard library sometimes has bugs: http://blog.adacore.com/formal-verification-of-legacy-code http://blog.adacore.com/formal-verification-of-legacy-code
  - pjmlp 9y ago
    Sure, every programming language can have bugs. However C gets the usual set of logical errors, common to any safe programming language, memory corruption caused by lack of checks on memory access and implicit type conversions, and 200+ cases of UB when taking advantage of full compiler optimizations. Reducing the amount of possible errors per line of code is already a plus, even if doesn't remove all of them.
  - touisteur 9y ago
    Note the article you're citing is going from Ada (already strong safety checks, but you can still write bugs, just not a whole class of them) to Spark2014, so formal proof of absence of runtime errors (first) and automated verification of functional properties. Even nicer, in a stdlib, so not a toy example and something to build on... You're showing (thanks !) how to go (with some effort, but not so much) from 'so much safer than C already' to 'no bug let's move on and maybe remove all the runtime checks to get C-like performance or better'. I'd say it looks pretty cool.

adrianN 9y ago

It's probably easier to use a language that has those guarantees already than trying to bolt them onto C. Those tools and coding standards are useful if you're constrained to using C for whatever reason, e.g. if you're on an embedded platform that only has a vendor compiler. For general purpose hardware you have a lot fewer headaches if you start with a language that was designed for safety.

margorczynski 9y ago
And I think the compiler/interpreter can optimize the code much better when the creators know that such constructs are available in the language itself