nanolith

7 ms·

31.
by nanolith 11mo ago
In C, you're correct. The problem is that, in C++, one must account for the fact that anything could throw an exception. If something throws an exception between the time that f is opened and f is closed, the file handle is leaked. Th
32.
by nanolith 1y ago
I'm living with heart failure. I have 20-30 years before I'll need a transplant, if I live a perfect lifestyle and keep my other health issues under control. Due to my other health issues, I am not a good candidate for a human hea
33.
by nanolith 1y ago
I have actually argued for the use of mailing lists for corporate engineering discussions. When that becomes the medium for code review or design discussions, there's a nice streamlined workflow. Further, it's practically trivial
34.
by nanolith 1y ago
If we mark any case that might be undecidable as a failure case, and require that code be written that can be verified, then this is very much sidestepping undecidability by definition. Rust's borrow checker does the same exact thing
35.
by nanolith 1y ago
It's not used more because it is unknown, not because it is difficult to use or that it is impractical. I've written several libraries and several services now that have 100% coverage via CBMC. I'm quite experienced with C de
36.
by nanolith 1y ago
The applicability of Rice's theorem with respect to static analysis or abstract interpretation is more complex than you implied. First, static analysis tools are largely pattern-oriented. Pattern matching is how they sidestep undecidab
37.
by nanolith 1y ago
Much to the chagrin of my mother, I made it a point about a decade ago to standardize old family recipes on "from scratch" versions. As part of the process, I also did some research on old recipes and fixed some of the corruption
38.
by nanolith 1y ago
Start with this. https://smt.st/SAT_SMT_by_example.pdf The algorithms behind SAT / SMT are actually pretty straight-forward. One of these days, I'll get around to publishing an article to demystify them.
39.
by nanolith 1y ago
There is a third category of memory and other software safety mechanisms: model checking. While it does involve compiling software to a different target -- typically an SMT solver -- it is not a compile-time mechanism like in Rust. Kani is
40.
by nanolith 1y ago
In some local areas where these urban legends were retold, that may be the case. My understanding is that the main reason why LSD usage faded was because the supply went down. There are plenty of factors here: reduced access to precursors,
41.
by nanolith 1y ago
It never happened. I've heard varying versions of this urban legend from the late eighties through to modern time. The reality is that an LSD trip can cause physical discomfort, especially toward the end. Sometimes this discomfort is s
42.
by nanolith 2y ago
The Ben Eater computer is an interesting starting point. With a few modifications, such as an extended program counter / address bus, a combinatorial ALU programmed in flash, and a few more registers, it can be upgraded to a more power
43.
by nanolith 2y ago
It's a clever use of assembler, but in production code, it's much better to use a bounded model checker, like CBMC, to verify memory safety across all possible execution paths.
44.
by nanolith 2y ago
and a very low-effort way to get a sense of superiority over others... literally anyone can learn in a few hours. I agree that it is a skill that is easy to learn. The same is true of IDEs. This isn't about skill or superiority, but
45.
by nanolith 2y ago
To each their own. With Vim, Unix is my IDE. I don't know about the recent interest in these editors that you mention. I've been using vi/Vim for the past 30 years. I take it to every project and job. My fingers already know
46.
by nanolith 2y ago
For C, I recommend CBMC.
47.
by nanolith 2y ago
I'm focused on C because a lot of our critical infrastructure is written in C. The Linux / BSD kernels, firmware, etc. It's also where my interest is. Model checked C is a good enough balance of cognitive load, safety, and ti
48.
by nanolith 2y ago
The reason why so few developers use model checking tools is because there is limited documentation out there for how to use them effectively. That is changing. Hell, I'm writing a book on the subject. These tools aren't difficult
49.
by nanolith 2y ago
> You're missing some other critical components: the developers, and the costs. No, I'm not. > If you come up with processes and tooling that is difficult to use widely, That's an unfounded assumption. The tooling and p
50.
by nanolith 2y ago
Yep. I'm writing up a response letter based on my own work with model checked C. It's not the language but the process and the tooling that matters. It is definitely true that the industry has been quite lax with memory safety, bu
51.
by nanolith 2y ago
Model checking employs abstract interpretation, so it's similar to static analysis. I hesitate to use the latter term, because it's often used to describe how linting works. This is significantly more advanced. The model checker t
52.
by nanolith 2y ago
So, the way I deal with this is to provide an exit condition in the loop that is triggered in a non-deterministic finite way by the model checker but that is not triggered at runtime. This allows for termination, which is required as part o
53.
by nanolith 2y ago
Yep. ESBMC and PolySpace both work for C++. I use CBMC for C. They run an abstract machine model through an SMT solver. Among other things, this abstract machine model tracks memory usage, UAF, aliasing, etc. With custom assertions, it can
54.
by nanolith 2y ago
Leave it to politicians to pit bull a language. Model checked C/C++ is memory safe. Had they reached out to a wider set of people for guidance, they'd have a more balanced report. I will agree that software safety -- not just memo
55.
by nanolith 2y ago
That's based on current estimates. It's impossible to know for certain, but there is a lot of C software out there. I'm a big fan of runtime mitigations. I use a few in my own work. WASM can help in some areas. But, bear in m
56.
by nanolith 2y ago
Jasmin has some great ideas. My goal in particular is to improve the tooling around C so that verification of C programs is easier. Because there are trillions of lines of C out there, I want to ensure that semi-automated processes can be d
57.
by nanolith 2y ago
Few languages provide such guarantees. But, there really was no way with this particular compiler to pass a hint to generate constant time code. Black box designs work until the knob or dial you need to control it isn't there. I would
58.
by nanolith 2y ago
That is reassuring. I hope that your team can build this web of trust, because it really is crucial. It is great to have a tool that allows ideas to be shared, but I think that consent regarding which ideas are shared or promoted is importa
59.
by nanolith 2y ago
Unfortunately, US case law is murkier. There have been some notable convictions of people using the old Freenet to search or host CSAM. However, the digital forensics used in these cases was pretty sketchy. If someone simply caching data fr
60.
by nanolith 2y ago
I'll refer you to my reply to a sibling comment. I'm hoping that I can build a more efficient means of doing similar work as with seL4, but without the 30 man year effort. They are on the right track. But, I think there have been

More ›