A theory for decades of C vulnerabilities

(strawberry9.github.io)

36 points by SilentLambda 6 days ago|21 comments

•

titzer 3 days ago

> A substantial portion of the initial manuscript was generated with the assistance of artificial intelligence. The author provided the underlying concept and creative direction and worked extensively with AI tools throughout the development of the book, selecting, restructuring, editing, rewriting, and refining the material. The final book reflects the author’s creative vision and editorial decisions.

I'm wondering how the author convinced the AI to forget about decades of prior work on describing programming language implementation and produce a work that seems to have no prior art.

•

readthenotes1 3 days ago

I was thrown off by the term "invariant" when the things called such are invariably... variant and often a source of dismay

•

hackthemack 3 days ago

I had similar? thought many years ago when strong typing became another one of the programming mantras touted on the internet.

Even dynamically type programming languages will layout what types the languages has. But that is usually the conventions built off of years of history, usually based on C.

But what if you wanted to define a custom type to use? Say you wanted to make type mysmallint, and it was an integer that is between 1 and 1000. Now, you can write up code to do this but it is not the same thing as declaring type int. *

*unless you are using Haskell, F#, or others I am not aware of.

What if you wanted to define a custom type that says this string only contains ascii characters? You can not easily define that as a type and pass it around the code. You have to write custom code and do checks.

•

kamma4434 3 days ago

This is one of the beauties of Clojure’s spec. You can define a ‘type’ that is a string which length is a prime number and contains only Ascii characters but ‘x’. To put those invariants in code and not in your head is so liberating.

•

matltc 4 hours ago

Don't know anything about clojure, but isnt this true with any language or library that implements schema validation? I'm thinking zod, for instance. Does clojure make it trivial?

•

rramadass 2 days ago

https://news.ycombinator.com/item?id=49381231

•

jakeinspace 3 days ago

Can't really have it all. If you want runtime assertions on your data/state, that has a cost. Nothing is stopping you from writing that logic out and having all your inputs and outputs sanitized for "semantic invariance". But if you want the language to implicitly do that, you're gonna have overheads. Pick a different systems language in that case, and deal with the tradeoff.

•

kelseyfrog 3 days ago

The author makes reference to making these invariants expressable via the type system, a compile time overhead, not a runtime overhead.

•

jakeinspace 3 days ago

Well, sure they make reference. Borrow checkers and memory ownership concepts, like in Rust, are pretty good at giving a very low overhead improvement over bare C pointers. But they're not as flexible. Shared memory complicates ownership rules. And invariably, any Rust program that involves real hardware will require dropping down into unsafe at some points. A safer program with an unsafe kernel is an improvement, don't get me wrong.

I'm not sure how a type system would "solve" arithmetic overflow / bounds dynamically, without expensive overhead (boxed types).

•

zbentley 3 days ago

I don’t think you have to reach for something as invasive as a borrow checker to handle most of these conditions. Bounds checks, for example, are rarely skipped intentionally in the vast majority of C programs; rather, they’re just skipped accidentally or performed incorrectly. Combine that with the extremely common and well-known compiler optimizations for BCE present in many compiled languages, and I don’t think C programmers get to trot out performance as an excuse for the language not supporting bounds checking by default, and providing escape hatches for people who really need to avoid it.

The same is true for overflow and unsafe math (tons of languages increase math and overflow safety on many paths without performance penalty, and baking that behavior into the type system with nondefault unsafe options is demonstrably tractable).

Hell, the prevalence of C static analyzers that warn about the vast majority of errors in these categories is proof that more safety is possible in C.

It’s not really about performance. It’s more the stubborn obsession with ABI compatibility at all costs and a pervasive lack of type system support and conventions relating to code reuse that hold C back.

•

matltc 4 hours ago

Well said. I get the sense that C is kind of ossified today, and that the whole point is its compatibility benefit. I wonder what even makes it into the next C standard? I think c99 was the last meaningful one. Everything else is offloaded to the compilers, God bless them. -Weverything

•

gregw2 3 days ago

Regarding the "expensive overhead of boxed types", do we just need more work at the hardware ISA level (with pointer tagging or NaN-boxing) and we need the hardware to be aware of those bits and handle them safely/properly via some minor extensions to RISC-V or Intel/AMD/Apple ISAs?

Or do we have to have completely new forms of hardware datatypes?

•

inguz 15 hours ago

Not mentioned in the article: macros, which surely are the traditional way to work with this in C and C++.

•

astrobe_ 3 days ago

Sorry but, ain't we tired of beating that dead horse again and again? We got it, C is a portable assembler and as such, is barely more "secure" than assembler. And yes, 50 years after C you finally have something as fast as it and more secure, congratulations.

•

rramadass 2 days ago

The article is conflating between two fundamental but different concepts;

1) Semantics of Language Constructs (part of Solution Domain) - These are just tools used to express any intention. You can make this as simple or powerful as you want.

2) Semantics of Programmer Intentions (part of Problem Domain) - These are the actual intentions expressed via a language according to the programmer's needs. Obviously no amount of language power can anticipate/provide-for all possible intentions.

In order to map (2) onto (1) we model problem approaches into distinct categories like Computation models (eg. Procedural/OO/Functional), Architectural models (eg. Monolith/Client-Server/Component) etc.

But the correctness of the above mapping depends only on the usage of rigorous formal logic to assert the intentions explicitly. This is why Dijkstra invented a simple language like GCL and taught how to verify your intentions in code using invariants/preconditions/postconditions and logical rules to mechanically transform a postcondition to precondition and thus derive a program based on intentions (expressed unambiguously as mathematical specifications).

A programming language can support the above at compile-time using types and/or at run-time using contracts but the fundamental problem of mapping Intentions -> Code can never go away. Hence this is what we should focus on learning. Once we are clear on this, mapping it onto any language (simple or complex) becomes comparatively trivial.