nanolith

21 ms·

211.
by nanolith 3y ago
GTA: Vice City was one of my favorite games. It was glitchy in an endearing way. While I'm no longer much of a gamer, I'm happy to see that Vice City is one of the game locations.
212.
by nanolith 3y ago
What you say is true, but you've inserted an inaccurate context with the quote. There is no guarantee that _direct access to system calls_ will last forever... Stability in the syscall API exists because Linux is a kernel that supports
213.
by nanolith 3y ago
That's a subtle point though. The kernel can't change defaults that break userland, nor can it change or eliminate features that would cause a breakage in userland. But, the kernel can certainly add an optional feature, like sysca
214.
by nanolith 3y ago
For most language runtimes, the minimal requirement for libc integration is to cover the standard Unix calls (unistd) which don't require specific memory management and typically just pass buffers directly from the caller to the kernel
215.
by nanolith 3y ago
Perhaps. To be fair, I'm not aware of anything on the horizon, other than the fact that OpenBSD has been showing off their pinning implementation. As long as you know it's a possibility, then the point of my original comment is me
216.
by nanolith 3y ago
A bad pattern according to whom? Most language runtime libraries import other system libraries as needed. For better or for worse, libc is typically considered to be a system library. It's something that every distribution or Unix flav
217.
by nanolith 3y ago
Direct syscall access is not something that is guaranteed in Unix derivatives. Linux is rare in that it provides a stable syscall API. Source compatibility is often only guaranteed when linked against libc or an equivalent low-level runtime
218.
by nanolith 3y ago
Many projects start this way. But, as per my comment, the assumption that direct syscall support will be maintained in future Linux distros is also risky.
219.
by nanolith 3y ago
This is interesting. Although, I think it's always useful to point out that runtimes that directly make system calls will have portability issues in other *nix systems. For instance, OpenBSD has recently restricted system calls to a si
220.
by nanolith 3y ago
> Unfortunately, unless you're careful, or have a test suite to make sure, it is the case. Respectfully, you are definitely conflating these concepts. First, a test suite can't replace a model checker. These are two very differ
221.
by nanolith 3y ago
> So you're saying humans are bad at writing software, but good at writing translations for model checkers? Nice strawman. However, that's not at all what I said. To restate in different words, even proofs can be incorrect. Eve
222.
by nanolith 3y ago
> This is unfortunately completely naive. Of course model checkers miss things. Perhaps you're thinking of a static analyzer which is something different. The ENTIRE POINT of a model checker is that it translates the program into a
223.
by nanolith 3y ago
seL4 primarily uses a proof assistant, which is a MUCH harder way to go about formal methods. It's thorough, sure, but for 80% to 95% of the average code base, model checking would work just fine. It's not a good metric to claim t
224.
by nanolith 3y ago
I know that it's a tough and often thankless job. People don't understand the real cost of pet care. Euthanasia is difficult, especially with pets. Pets are very much like children. I make it a point when calling on a veterinarian
225.
by nanolith 3y ago
I started writing software as a child, in the eighties. I only had access to various forms of BASIC and machine code. I switched to C in the early nineties, when I got access to Turbo C in middle school. Later, I got access to Minix, BSD, a
226.
by nanolith 3y ago
CBMC is subtle and will require some code changes to use effectively. The real key for using it, in my opinion, is to isolate individual classes and functions. Avoid instrumenting code with recursion and loops, and focus on defining and ver
227.
by nanolith 3y ago
Thanks. That is useful. I would suggest looking into CBMC and similar tools as well. Model checking is incredibly useful.
228.
by nanolith 3y ago
Given that their entire code base is written in C++, and switching to a different language would be a significant retooling for the team, I think it's reasonable to assume that it did not. Language choice is rarely made on the grounds
229.
by nanolith 3y ago
Shiu's paper is a nice improvement over Crowley's findings (here: http://www.ciphergoth.org/crypto/solitaire/ ). I've taught folks to use this cipher, then showed them Crowley's analysis. It&#x2
230.
by nanolith 3y ago
seL4 has seen use in military projects, including UAVs and drones. It's been endorsed by the Linux Foundation. I wouldn't really call it an academic proof of concept at this point. Regarding logic problems, I've tested GPT-4
231.
by nanolith 3y ago
The existence of seL4 and its ability to be used in real projects certainly proves that formal methods has been effectively used to improve safety and security in shipping products, which was the question you asked if I understood it correc
232.
by nanolith 3y ago
If, by "here", you mean AI, the answer is "unlikely". I was replying to the GP's assumption that such technology exists for traditional software. It does. CBMC exists today, and can be used to enforce function contr
233.
by nanolith 3y ago
LLMs and other generative AI methods are nowhere near replacing the need for better reasoning about software, especially in safety critical systems.
234.
by nanolith 3y ago
That's not what I claimed. The parent poster was talking about non-AI applications. Regarding their use today, model checking is indeed quite usable -- today -- for verifying function contracts. It is more difficult to use model checki
235.
by nanolith 3y ago
> That's probably possible now. It's definitely possible now. Formal methods continues to shift from the theoretical, academic, and difficult to the practical. There are model checkers based on SMT solvers that can be used toda
236.
by nanolith 3y ago
It's practically impossible to pick names that haven't been used for something else. I've taken to using the contraction of random amusing phrases when I want a unique name, but this isn't any better. Just fun (for me).
237.
by nanolith 3y ago
First, I'm no expert on this. While I do contribute patches to various OSS projects, I'm not an insider in any. I possess some old-school netiquette and I've gone through plenty of commercial projects, so there are enough sim
238.
by nanolith 3y ago
It's fine to bristle about underhanded evangelism (e.g. "Use Rust instead of C, because C is a foot cannon and Rust is perfect"), but that's definitely not the case here. This is a reasonable critique of the common C pit
239.
by nanolith 3y ago
I think that the use of an escrow service would be an excellent idea. There's some complexity to deal with in order to make this fair for both companies and consumers, but I think that these difficulties are surmountable. An open sourc
240.
by nanolith 3y ago
To add to previous similar comments, I think that one of the best ways to ensure that security updates are provided is to ensure that manufacturers either commit to continuous security updates, or after a minimum sunset period during which

More ›