nanolith

10 ms·

61.
by nanolith 2y ago
Indeed it is. What I'm working toward is a more efficient way to do the same, that doesn't take the touted 30 man years of effort to accomplish. I'm working on a hybrid approach between SMT solving and constructive proofs. Mo
62.
by nanolith 2y ago
One area that I have been exploring is building equivalence proofs between high-level specifications, an implementation in C, and the machine code output from the compiler. I'm still very early in that work, but one of my hopes is to a
63.
by nanolith 2y ago
While Locutus is an improvement on the previous Hyphanet model, I'm still concerned about the caching model. In Hyphanet, data would be cached the more it was used, and peers connected over multiple hops. This had the potential to caus
64.
by nanolith 2y ago
It's a form of abstract interpretation. The code is compiled to a constraint problem in an SMT solver. There is definitely a performance impact here, which is why it is important to decompose the program and verify it function by funct
65.
by nanolith 2y ago
1. Of course it can. My model checks on function contracts and invariants run for every function. If a function fails this contract or invariant, the overall build fails. Does it matter that this is a separate build step than the compilatio
66.
by nanolith 2y ago
I appreciate your opinion. It's not possible to hold a nuanced conversation about model checking in general or in C in particular in the comments of HN. I'd need much more space. But, I can summarize. CBMC's abstract machine
67.
by nanolith 2y ago
> Unless you have some insider info, I think you’re oversimplifying why Linux is giving Rust a chance. Not really. Linus Torvalds has been quite open about this topic, and it has been covered extensively on LWN. > Also, model checking
68.
by nanolith 2y ago
It is quite practical. I'm actually planning a book on the subject. The reason why some Rust enthusiasts have been experimenting with Rust in the Linux kernel is because they are passionate about Rust, and kernel maintainers are lookin
69.
by nanolith 2y ago
If you want those things, you don't want C. Pick a reasonable higher level language you like that makes those decisions for you. My comment was not to imply that somehow C is superior to X, Y, or Z, but rather to point out that the saf
70.
by nanolith 2y ago
The compiler really doesn't have the opportunity to simulate every possibility of code. It's not just the matter of whether the function is safe, but every possible use of the function, which the compiler may not see when it is fo
71.
by nanolith 2y ago
That used to be true, but now we have reasonable model checking tools for C. It's possible to write safer C without the cognitive load of Rust. https://www.cprover.org/cbmc/
72.
by nanolith 2y ago
Shooting invasive species is definitely legal in Florida assuming that you have permission of the land owner or are otherwise in a location where shooting is allowed (i.e. not in a municipality that bans the gunfire). It has to be done huma
73.
by nanolith 2y ago
I'd recommend using FreeBSD as your first BSD. It has a more recent version of ZFS integrated in the kernel than NetBSD. OpenBSD does not have ZFS support; it's a direction they chose not to take for security and simplicity reason
74.
by nanolith 2y ago
That is really cool. I've been threatening to do something like this for years. Thanks for this!
75.
by nanolith 2y ago
I've never been comfortable drawing or drafting with GUIs. This is true for "drawing" graphics, laying out boards, or building 3D models for printing or CNC. OpenSCAD has been invaluable to me. Usually, I'll hand draw wh
76.
by nanolith 2y ago
The formal methods nerd in me is happy to see HOL Light being used to formally verify this implementation. I'm curious to see how closely their abstract machine models follow specific machine implementations. OOO, speculation, and deep
77.
by nanolith 2y ago
Not yet, but very soon. My previous work was done for employers and involves code that is not free to distribute. I am currently working on some blog articles to cover a web application written in model checked C. Once that is done, and onc
78.
by nanolith 2y ago
It's certainly still being used. I use bounded model checking, which performs a kind of symbolic execution using an SMT solver. For more complex things that aren't as easy to model check, such as the formal verification of a deepl
79.
by nanolith 2y ago
I agree, and it's nice to have Python bindings for it.
80.
by nanolith 2y ago
You can set weights for each soft constraint to control how easy they are to break.
81.
by nanolith 2y ago
You can set soft and hard constraints. Soft constraints can be broken if the system is unsatisfiable otherwise. For instance, by default, this config sets a soft constraint that two people must be at the desk, and a hard constraint that no
82.
by nanolith 2y ago
I wrote a simple DSL that she can use. She knows some HTML and basic scripting, so as long as the rules are easy to express and she has good examples, she can tweak the rules herself. I just hacked up a little shallow embedding via lex&#x2F
83.
by nanolith 2y ago
Nice work. Some things that I think work well for SMT solvers: 1. Bounded model checking for source code. 2. Finding solutions to constraint problems. 3. Design rule checking for hardware layout and logic gates. Recently, I built a simple s
84.
by nanolith 2y ago
I don't. Passion is good, and I'm glad we can have a passionate discussion while remaining civil. We both want the same thing: safer software.
85.
by nanolith 2y ago
> I, too, enjoy sci-fi I was characterizing these hardware changes as being fantasy, so I'm glad you agree. > So I'd say if the said CBMC, and likely other tools in the same area, has more or less failed if it could not c
86.
by nanolith 2y ago
Well, that's something I hope to change. The tools required to write safer software exist. They just aren't widely distributed yet. I can say, without ego, that I'm a reasonably good software developer. But, it is the tooling
87.
by nanolith 2y ago
There is nothing wrong with defense in depth. But, this is not where things stop. I make extensive use of bounded model checking in my C development. I also use privilege separation, serialization between separate processes, process isolati
88.
by nanolith 2y ago
Yep, but we have to deal with what we have. For better or for worse, C remains where it is. We can either use process and tools to improve existing C, or throw our hands up. I prefer to work toward fixing what is. We are unlikely to see thi
89.
by nanolith 2y ago
That's a rather cynical interpretation of these initiatives. CHERI, for instance, has been in development for twenty years. It predates the general availability of open source tools like CBMC or languages like Rust. But, that doesn&#x2
90.
by nanolith 2y ago
> The amount of people using stuff CBMC is like trying to boil the ocean. That's like saying, "Getting everyone to use Rust or TDD or X is like trying to boil the ocean." It's impossible to solve all things for all

More ›