3 ms·
> The reason is that it currently still is hard and not worth the effort for >99% of software. That sure sounds like they're delusional to me. Take the vulnera
by tialaramex 3y ago
> The reason is that it currently still is hard and not worth the effort for >99% of software.
That sure sounds like they're delusional to me. Take the vulnerability of smartphones to various vulnerabilities in image codecs over the past few years. That's a solved problem, that's what WUFFS is for, and yet of course Apple doesn't use WUFFS-the-language, or even WUFFS-the-library, they're content that if they can just fix all the bugs in their C++ it'll be fine†. Even Google, which is paying the main author of WUFFS, doesn't use most of it, because hey, they've got handrolled (read, probably riddled with security holes) C++ code... they use his GIF implementation, they might adopt more later, but they haven't yet.
All WUFFS is doing is saying "Oh, if we run a proof checker during compilation we can solve this narrow problem completely" and yet that's apparently too hard. We're not talking about teaching your programmers Coq here or implementing the Principia in Haskell, but what we see over and over is that people would rather cobble together crap that compiles but is garbage and then go home for the day.
† To be fair to Apple their medium/long term plan is to Rewrite It In Swift, but while that's an improvement it is not a guarantee of safety, it's a half measure in some unknowable future.
- staunton 3y agoIt doesn't sound like you necessarily disagree. Maybe we use different meanings of "worth the effort"? I meant it in terms of money that a company can save or make from deciding to expend that effort. You also have an additional cost in terms of "risk" that the effort does not yield desired results. So "they're delusional" would only be true if the people deciding this seriously overestimate the effort to verify something or seriously underestimate the benefits. Do you think that's true in general? Or even in the examples you cite? It seems like Apple and Google know what WUFFS is and what it can and cannot do, so they understand the effort. The maximum conceivable benefits in the cases you mention would be "no security vulnerabilities in said code". I'm not sure that is seen as a huge benefit by those in charge. Even rewriting that stuff in Rust (or even Swift) would significantly reduce the probability of weaknesses being exploited. Nobody seems to think that's worth the effort. The "marketing pitch" of WUFFS is: "as safe as Go or Rust, roughly speaking, but as fast as C, and that can be used anywhere C libraries are used". So, presumably, Rust and Go are equally and sufficiently safe, "roughly speaking"? And Rust is neither fast enough nor easy enough to integrate with C code (despite being good enough for drives in the Linux kernel)? This sales pitch makes it clear that the people behind WUFFS are keenly aware that "safety" alone doesn't sell. This problem is generally more endemic of software security in general. The cost of security issues is usually not borne by the people who decide how much to invest into security. Also, security does not contribute to profits, it is only a cost center. By contrast, when you have really important code and you bear the cost of mistakes and outages directly, formal methods are being used where it can be done straightforwardly. AWS and some cryptocurrencies (for whom security and correctness is an above-average part of their sales pitch) have prominent uses.