this post was submitted on 14 Feb 2024
20 points (95.5% liked)

Permacomputing

640 readers
2 users here now

Computing to support life on Earth

Computing in the age of climate crisis is often wasteful and adds nothing useful to our real life communities. Here we try to find out how to change that.

Definition and purpose of permacomputing: http://viznut.fi/files/texts-en/permacomputing.html

XMPP chat: https://movim.slrpnk.net/chat/lowtech%40chat.disroot.org/room

Sister community over at lemmy.sdf.org: !permacomputing@lemmy.sdf.org

There's also a wiki: https://permacomputing.net/

Website: http://wiki.xxiivv.com/site/permacomputing.html

founded 1 year ago
MODERATORS
schmorpel
20
The ever-growing problem of ever-growing codebases (www.theregister.com)
submitted 8 months ago by poVoq to c/permacomputing
10 comments fedilink hide all child comments
you are viewing a single comment's thread
view the rest of the comments
[–] perestroika 4 points 8 months ago* (last edited 8 months ago) (4 children)

These projects are so incomprehensibly vast that no human mind can comprehend even one small isolated subset of the entire thing.

Which means - no human mind can trust them either, and no human programmer alone can conduct a security review.

Which means they should not be trusted, and should be considered insecure - unless they can be carefully isolated from the environment so that only a trusted surface is exposed.

My ideal project size: something that an average coder can read in a week or two, and come back to their (possibly anarchist) colleagues saying: "this code looks reliable and won't be leaking buckets".

[–] demesisx@infosec.pub 8 points 8 months ago* (last edited 8 months ago) (2 children)
[–] perestroika 2 points 8 months ago (1 children)

Some quite interesting articles, thank you - I read two and quick-scanned some more.

Formal verification seems the way to go if you do build a system top down.

What tends to ruin the day is when you need to use components of somewhat random origin. In addition to the OS, you have device drivers, often supplied by vendors who cannot be bothered to go beyond the minimum, you have applications, some of which are legacy and some poorly maintained, written in 12 different programming languages and using 12 different network protocols, some having great traction (thus being necessary) but designed as they were in those days...

...in a chaotic environment, formal verification seems like a big burden to carry. It therefore seems like a method which a rich organization can afford, but not something a small or poor organization can use.

For smaller players, I think minimizing and simplifying their tools may be more accessible. If one can throw out most components, limit the contact surface to something small, use the simplest tools on that surface and make their review easier - I think one can get reasonably high assurance without all-encompassing verification...

...but then again, if you build a manned aircraft, spacecraft or submersible, or a medical apparatus or life support system, then I think formal verification would be a really good idea. :)

[–] demesisx@infosec.pub 6 points 8 months ago* (last edited 8 months ago)

Thanks for taking a look. I agree that it is REALLY challenging (and currently impossible) to maintain that kind of formality in most codebases. Where it matters, though, it really helps.

I got interested in formal verification in the context of a future (currently vaporware 😅), formally verified version of the Cardano node running on a Formally Verified flavor that utilizes the RISC-V architecture. I’m just trying to put it on the white beards’ radar over there at IOG (it’s WAY out of my wheelhouse and perhaps even many of theirs too!) because this kind of thing, if fully open source (as that whole codebase is), could make this level of sophistication much more achievable by mere mortals.

Another amazing company that got me into this level of sophistication was Runtime Verification. If you like looking at projects that are absolutely world-changing, look into their K framework. They’ve created a whole framework for formally specifying whole programming languages (and even the LLVM!) and can pretty much use it as a Babel Fish for converting code from one programming language to another, which I always thought was impossible. But if there’s any outfit that could accomplish it, it might be those geniuses who regularly work with companies like NASA and aerospace behemoths.

load more comments (1 replies)