nanolith

14 ms·

91.
by nanolith 2y ago
There are no silver bullets. But, that doesn't mean that we should dismiss tooling that is not well understood in order to chase unrealistic goals, like rewriting extant code bases in a different language to achieve security goals. Or,
92.
by nanolith 2y ago
> The proven fact that the said technology has failed its purpose, How, because other solutions are being explored? That's not due to a failure of one thing, but because both defense in depth and a desire to fix existing systems w
93.
by nanolith 2y ago
Bounded model checking has changed things. C on its own can't solve these problems. Likewise, Rust on its own -- while it can solve memory errors -- can't demonstrate safety from all errors that lead to CVEs. Practical formal meth
94.
by nanolith 2y ago
Respectfully, that's a rather extraordinary claim. There are model checkers that use separate specification languages, but there are also model checkers embedded in the host language. CBMC translates C -- the same language -- to an SMT
95.
by nanolith 2y ago
> Rust clearly does Until it exists at the kernel layer, the firmware layer, the runtime library layer, and the application layer, these issues still exist. CVEs come out weekly for memory errors in Linux, in firmware, in operating sys
96.
by nanolith 2y ago
> That's not "in reality", that's "in theory". Because in actual reality, people still write the good old buffer overflow bugs to this day. That's because while the technology exists, it is not widely c
97.
by nanolith 2y ago
You're welcome. I've been meaning to write a blog article on the subject, because it is a subtle thing to get working. Think of shadow functions as the specifications that you are building. Unlike proof assistants or Frama-C, you
98.
by nanolith 2y ago
CBMC works best on functions, not programs. You want to isolate an individual function, then provide shadows of the functions it calls. The shadows should have nondeterministic behavior (cover every possible error condition) and otherwise f
99.
by nanolith 2y ago
These studies aren't wrong. But, that's also because neither Microsoft nor Google make use of practical formal methods in practice. Both have research teams and pie-in-the-sky projects, not dissimilar to this DARPA project. But,
100.
by nanolith 2y ago
> A huge investment. If you are going to do that then you might as well just move to Rust. People say that, but the people who say this rarely have any practical experience using CBMC. It's very straight-forward to use. I could teac
101.
by nanolith 2y ago
> No chance. CBMC is amazing, but have you actually tried formally verifying a "real" program? Yes. Every day. It's actually quite easy to do. Write shadow methods covering the resources and function contracts of called fu
102.
by nanolith 2y ago
I'm personally not a fan of "rewrite the world in Rust" mentality, but that being said, if one is planning to port a project to a new language or platform, mechanical translation is a poor means of doing so. Spend the time pl
103.
by nanolith 2y ago
kani certainly could be extended to have better async / await support. But, I think this is a larger engineering problem. The value of code that has been verified using an existing model checking tool is greater than the value of code
104.
by nanolith 2y ago
Threading and async are an issue with the current CProver core. But, much of that can be simulated by writing helper functions that get shadowed during the model checking. It's simply not possible to make a bounded model checker work o
105.
by nanolith 2y ago
You can write these checks as assertions in your regular source language. It's no more difficult than writing runtime parameter checks, really. There are some complexities, to be fair, but these are mostly around the performance of the
106.
by nanolith 2y ago
Yep. JBMC is part of the CProver / CBMC family.
107.
by nanolith 2y ago
In my opinion, most developers should be using bounded model checking if available for their language / platform. This is certainly true for C, Rust, Java, and others. I consider bounded model checking to be "formal methods lite&q
108.
by nanolith 2y ago
"On the Dangers of Stochastic Parrots" (doi:10.1145/3442188.3445922) is a great introduction to this, even with its flaws. I also recommend Mitchell 2023 (doi:10.1073/pnas.2215907120) and Niven 2019 (arXiv:1907.07355) as
109.
by nanolith 2y ago
You missed important context there. In particular, "These LLMs are being trained on data sets with bad results and bad code with no real way to tell the difference." A couple dozen bad SO articles can easily poison the results of
110.
by nanolith 2y ago
Such a model has not yet been invented. Certainly, a generative model such as a large language model is unlikely to gain the ability to reason about these answers. LLMs are a step on the path toward better human/computer interaction, b
111.
by nanolith 2y ago
From the article: "Our relative lack of skill at investigation becomes clear when we look at the accuracy rate of StackOverflow answers. For the amount of sass you see on that platform, you’d expect the programmers to at least be right
112.
by nanolith 2y ago
Early in my career, I wrote a LEAPS based rules engine for managing business rules when deciding how to pack orders into boxes across multiple warehouses. As part of it, I also wrote a heuristic for approximating solutions to the 3-dimensio
113.
by nanolith 2y ago
Yet another reason why I'm not a fan of modern cars. The trend is going against the consumer. I recently had to spend $1200 to replace a headlight because my car was designed so that it's impossible to perform such a simple repair
114.
by nanolith 2y ago
Most of their monorepo code I came across used 80 columns. But, I can't speak for all of it. Google has a LOT of code. Either way, if Google and other companies can do what they do in 80 columns, I think it's a fair constraint. Wh
115.
by nanolith 2y ago
On my 4K monitor, I use 4-5 vertical splits and 2-3 horizontal splits. The 80 column rule makes each of these splits readable, and allows me to see the full context of a chunk of kernel code or firmware at once. It has nothing to do with &q
116.
by nanolith 2y ago
I'm hoping to purchase land and semi-retire over the next four years. My wife has an interest in beekeeping, and this is exactly the sort of thing we'd love to do.
117.
by nanolith 2y ago
If the tool exists and has minimal overhead, I don't think it is a matter of permission but a matter of necessity. CBMC adds about 30% overhead over just unit testing, in my experience. It does require a different idiomatic programming
118.
by nanolith 2y ago
Unfortunately, I have not found any good tutorials. If it helps, I plan on writing one very soon.
119.
by nanolith 2y ago
I have been using CBMC to formally verify C for six, make that seven years now (edit: time flies). The latest release is actually pretty good. The secret to model checking is to understand that you're building and verifying a specifica
120.
by nanolith 2y ago
My wife is a librarian. The elephant in the room here is that patrons are shifting toward a preference for digital distribution. However, Fair Use has not caught up. So, libraries end up spending a large portion of their operating budget &q

More ›