it's also a very limited version of C, without concurrency, dynamic memory allocation, or goto, and you can't even take the address of local variables!
Current project (business backend server in C++) that would qualify for attack sits behind NGINX. Looking at the logs I see all kinds of attempts related to Wordpress, PHP, etc. etc. Also we use 3rd party protection on production before NGINX.
Since the server exposes proprietary JSON API with what I would say extreme validation before trying to actually do anything nothing that seems to be illegal gets in.
I mean it is not 100% guarantee as nothing else in our lives but so far nothing extraordinary (keeping my fingers crossed).
if you see it in the logs, that seems like bots looking for low hanging fruit. what about focused attacks by sophisticated adversaries? here, a heap buffer overflow in a c++ library is a major part of enabling rce https://en.wikipedia.org/wiki/Xpdf
Capabilities are a good way to mitigate this problem, yes. At minimum cap_std::fs would prevent "../" attacks.
"../" attacks are also just way less of an issue when you shove your programs into minimal containers, which at this point is more or less standard practice.
> Rust ... "Isn't Really Safe" because you can get into a point where memory is corrupted
i dare you to find memory corruption in safe rust that isn't already on an issue tracker.
> Saying that a language is either safe or unsafe implies that the "safe" language is actually safe while the "unsafe" language is completely deadly.
tell that to the people who got owned by https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-i... , most likely human rights activists targeted by less-than-savory regimes. memory corruption bugs are so frequent that it is possible for nso group to sell to pretty much any regime, and not forced to be classified as top secret information.
(To be clear, I’m not saying that there’s no issues that aren’t in the tracker yet. But there are a bunch of them that are. More will absolutely be found as time goes on, that’s just how these things are.)
what do you mean invalidated? the point of proofs is that they will be still be as true today as they will millenia into the future. pythagoras' theorem is just as true today as it was millenia ago.
do you know if anyone has used frama-c to verify properties as "deep" as those done by seL4, like functional correctness and integrity, rather than a "shallower" property like memory safety or absence of crashes?
Yes, Frama-C uses a plugin architecture, and there are plugins to verify all kinds of things, including functional correctness. The Frama-C tutorials page,
Also, it is less effort to write bug-free code in OCaml than C. The Coq/Gallina proof assistant even has an OCaml-extraction (and also Haskell-extraction) feature where you extract runnable code from a formally verified algorithm in the Gallina specification language. (It's generally easier to proof theorems about code in the theorem prover itself, go figure.) Most of these C verification tools are written in OCaml, not C, with varying levels of assistance from Coq/Gallina.
The main reason the functional languages make it easier is because you generally execute side-effect free functions on data structures to give them the mathematical property you want. For example, you execute a lexicographical sort function on a list of strings and then the strings in the list all satisfy the mathematical property of a total ordering. You don't have to do any reasoning about the "in-between state" where pointers under the hood are being manipulated, and you don't have to add pre-conditions and post-conditions about the global environment if the code is side effect free and does not access non-local memory.
"Big" software is mostly not difficult algorithms, but writing boilerplate glue code that connects the inputs and outputs of algorithms/functions that are usually written by someone else. Frama-C can definitely verify the boilerplate for "big" software, this is actually easier than verifying data structures and algorithms, which requires knowing the key property to get the prover to see that the algorithm always makes progress toward a solution. Once you have the contracts set up for calling a function, Frama-C will enforce that the contract is always met.
The CompCert verified C compiler is "big" software, but not actually written in C, rather OCaml and Coq/Gallina.
Yes, a compiler written in C could be verified with Frama-C, but "verifying in Frama-C" for something that hard (i.e. has many proof steps that cannot be automated) really means verifying in a proof assistant that can interact with Frama-C that understands ACSL, and Coq is usually used. And indeed, the loop invariants you mention usually cannot be automatically proved and must be proved manually, which is why there is such a learning curve to Frama-C. I first started using Frama-C without having used Coq/Gallina/OCaml, and I began to learn them simply because I hit a roadblock with Frama-C where I couldn't really progress without a deeper understanding for why automatic proving fails when it fails, why the error messages when automatic proving fails often aren't terribly helpful, what the current limits of automatic proving are, how the automatic proving actually works under the hood, etc.
Coq has been used to formally verify a large body of classical mathematics. Coq can 'understand' what a prime number is and can be used to prove that there are infinitely many primes, can prove that sqrt(2) is irrational, etc. Coq can prove a recursive solver for the Towers of Hanoi actually solves the problem, etc. And thus Coq can prove a C program to solve the Towers of Hanoi correctly solves the problem, because Coq can reason about C programs.
I've been slowly working through the Software Foundations series on using Coq/Gallina:
Another poster mentioned CBMC which I just started playing with. It is much less powerful than Frama-C, there isn't the ACSL specification capability and theorem proving, but it is much more automatic and much faster to get started with. For many cases if I just want to verify that a certain C file frees all its mallocs, doesn't have out-of-bounds accesses, and that all obviously bounded loops terminate, CBMC is much easier. Also, like Frama-C, it converts C functions into "goto programs" (removes the syntactic sugar of 'for' and 'while' loops to obtain a more pure Control-Flow-Graph (CFG)) for certain forms of analysis, and when I first encountered this in Frama-C there was no explanation why, whereas the manual for CBMC actually has an excellent gentle introduction:
