3 ms·

Immediately you mentioned memory safety, Rust is the language that came to mind. Memory safety is indeed important, but I find it hard to believe that in the fu

Immediately you mentioned memory safety, Rust is the language that came to mind. Memory safety is indeed important, but I find it hard to believe that in the future, ~80% of mainstream system tools will be migrated from C/C++ to Rust. Is it possible or has there been any attempts to write standalone tools that are able to check before compile-time that a particular C/C++ program won't have buffer overflows/dangling pointers? I don't expect such a tool to catch everything, but it should at least be able to track most of such bugs. EDIT: typos

steveklabnik 9y ago
https://github.com/Microsoft/GSL https://github.com/Microsoft/GSL is an attempt at something like this. The Core Guidelines have been in development for a long time now; and they do only catch a subset of issues. I'm all in favor of making languages safer overall though!
xamuel 9y ago
Detecting 100% of buffer overflows with 0% false alarms, would require solving the Halting Problem. For applications that demand both maximum speed as well as maximum security, the best solution is probably something like a C compiler that requires the code to be accompanied by formal proofs of defined behavior. Even this will necessarily sacrifice speed in a theoretical sense, because there are certain problems for which the fastest solution is safe but can't be proven safe within (PA/ZF/ZFC/insert any consistent foundation of mathematics you like). Eventually we'll have people writing fast programs and proving their soundness using large cardinal axioms which might or might not actually be true. Then someday one of those large cardinal axioms will turn out to be inconsistent [1] and suddenly some "proven" code will be proven no more. [1] https://en.wikipedia.org/wiki/Kunen%27s_inconsistency_theorem https://en.wikipedia.org/wiki/Kunen%27s_inconsistency_theore...
- andrewflnr 9y ago
  Why would you need large cardinal axioms to prove a program correct?
  - xamuel 9y ago
    I used large cardinal axioms as [the canonical] example of any axiom stronger than standard mathematical foundations. A contrived example: there are certain large cardinal axioms that imply the consistency of ZFC. Thus ZFC cannot prove those axioms unless ZFC is inconsistent (Godel's incompleteness theorem). Consider the following problem: "If ZFC can prove 1=0 in n steps, output 1. Else, output 0." A naive solution would brute-force search all ZFC-proofs of length n. A faster solution would be: "Ignore n and immediately output 0." This is correct, because ZFC never proves 1=0. You could formally verify the correctness by using certain large cardinal axioms, but not using raw ZFC.
AgentME 9y ago
A system that guarantees you full memory safety in C/C++ would probably force you to use programming patterns that are much easier in Rust. At some point you'd essentially be writing Rust code in C/C++ with worse tooling and worse syntax-fit.
- andrewflnr 9y ago
  Not necessarily. Rust's ownership system is really quite conservative, to the point of not really letting you write doubly linked lists (without unsafe or using indices or something). A memory safety system for C/C++ that lets you prove cyclic pointer structures safe, or even helps you safely implement GC, is probably possible and would be quite cool. We'd probably jump at the chance to use something similar for unsafe Rust, too.
Pete_D 9y ago
Frama-C lets you prove all sorts of useful properties about C code, including memory correctness. (Actually writing the proofs is a lot of work though.) https://frama-c.com/acsl.html https://frama-c.com/acsl.html
WalterBright 9y ago
D is also memory safe, and it has been modified to make it possible to gradually migrate a C program to D. https://dlang.org/blog/2017/08/23/d-as-a-better-c/ https://dlang.org/blog/2017/08/23/d-as-a-better-c/

steveklabnik 9y ago

https://github.com/Microsoft/GSL https://github.com/Microsoft/GSL is an attempt at something like this. The Core Guidelines have been in development for a long time now; and they do only catch a subset of issues. I'm all in favor of making languages safer overall though!

xamuel 9y ago

Detecting 100% of buffer overflows with 0% false alarms, would require solving the Halting Problem. For applications that demand both maximum speed as well as maximum security, the best solution is probably something like a C compiler that requires the code to be accompanied by formal proofs of defined behavior. Even this will necessarily sacrifice speed in a theoretical sense, because there are certain problems for which the fastest solution is safe but can't be proven safe within (PA/ZF/ZFC/insert any consistent foundation of mathematics you like). Eventually we'll have people writing fast programs and proving their soundness using large cardinal axioms which might or might not actually be true. Then someday one of those large cardinal axioms will turn out to be inconsistent [1] and suddenly some "proven" code will be proven no more. [1] https://en.wikipedia.org/wiki/Kunen%27s_inconsistency_theorem https://en.wikipedia.org/wiki/Kunen%27s_inconsistency_theore...

andrewflnr 9y ago
Why would you need large cardinal axioms to prove a program correct?
- xamuel 9y ago
  I used large cardinal axioms as [the canonical] example of any axiom stronger than standard mathematical foundations. A contrived example: there are certain large cardinal axioms that imply the consistency of ZFC. Thus ZFC cannot prove those axioms unless ZFC is inconsistent (Godel's incompleteness theorem). Consider the following problem: "If ZFC can prove 1=0 in n steps, output 1. Else, output 0." A naive solution would brute-force search all ZFC-proofs of length n. A faster solution would be: "Ignore n and immediately output 0." This is correct, because ZFC never proves 1=0. You could formally verify the correctness by using certain large cardinal axioms, but not using raw ZFC.

AgentME 9y ago

A system that guarantees you full memory safety in C/C++ would probably force you to use programming patterns that are much easier in Rust. At some point you'd essentially be writing Rust code in C/C++ with worse tooling and worse syntax-fit.

andrewflnr 9y ago
Not necessarily. Rust's ownership system is really quite conservative, to the point of not really letting you write doubly linked lists (without unsafe or using indices or something). A memory safety system for C/C++ that lets you prove cyclic pointer structures safe, or even helps you safely implement GC, is probably possible and would be quite cool. We'd probably jump at the chance to use something similar for unsafe Rust, too.

Pete_D 9y ago

Frama-C lets you prove all sorts of useful properties about C code, including memory correctness. (Actually writing the proofs is a lot of work though.) https://frama-c.com/acsl.html https://frama-c.com/acsl.html

WalterBright 9y ago

D is also memory safe, and it has been modified to make it possible to gradually migrate a C program to D. https://dlang.org/blog/2017/08/23/d-as-a-better-c/ https://dlang.org/blog/2017/08/23/d-as-a-better-c/