/tech/ - Technology★

there is no proof for x86

OP is an insane shill who regularly posts these threads btw

>>1027197

x86_64's functional correctness proofs are complete, slowpoke.

>>1027196 (OP)

>Why aren't you using an unhackable kernel, /tech/?

Why aren't you? The screenshot in your OP is from the website.

I can give it a try but it is not the first time I see something claiming to be absolutely bug free and safe

>>1027236

If I understand it correctly, it's just running Tiny Core Linux on top of an seL4-based VM. I'm not sure what the setup is supposed to protect against.

Great. Where is the unhackable hardware?

>>1027242

Well, virtulization inherently adds security, i.e. ambiguity between the kernel and the hardware. It could limit the tiny-core kernels access to the hardware... however, virtulization also inherently adds certain vulnerabilities.

I agree, it doesn't seem that great.

>>1027210

They rely on the assumption that the memory coherency model is totally known and shit like this, I guess.

Is it really unhackable or just marketing? Even then you could still hack the other parts of the system.

>>1027269 Yes, it also can be hacked. Actually, all systems can be hacked if they are made by human beings!

seL4 is like having just the steering wheel of car. You can't do anything with it, it just a small part of a bigger thing. Of course you can formally verify it, it's like formally verifying that a single nail in a house is made of metal.

Even Genode, which is based on L4, is just a framework for operating systems, a tool for building more complex OSs.

If you say this is unhackable, you need to fucking leave.

Formal verification is a great step forward, but you, OP, are a verified fuckwit. Go away until you realize how stupid your post was. If you are trolling then you did a 7/10 job but fuck off anyway.

>>1027196 (OP)

Literal NSALinux.

>>1027269

>Well, virtulization inherently adds security,

Theo disagrees. And even if he's wrong, there are many attacks that this scheme won't protect against anyway. If, for example, you're using the Tor Browser Bundle and there's some exploit of the browser that exposes your real IP address, this won't protect against that. I don't even think it will protect against things like privilege escalation inside the VM. So unless you're booting a clean VM every time and not saving state between reboots, you just end up with a rooted VM.

And if you are using some amnesiac VM setup, why bother with this over Xen or anything else?

What's the threat model that Sculpt addresses?

>unbackable kernel

Yeah right, like anyone who's ever sold something as 'unhackable' hasn't been completely full of shit

Putting the 'unhackable' bullshit aside, I'm more interested of seL4 as a microkernel. How is it compared to previous attempts at creating microkernels? I heard it's kinda fast, but I don't know if it's fast enough to be a serious alternative to monolithic ones.

I'm a brainlet so explain to me in simplest terms how can an unhackable kernel exist and why other software can't be unhackable like seL4 as well?

>>1027595

and oh could future DRM schemes borrow some ideas from seL4 and how catastrophic would that be?

>>1027563

Well seL4, as its name implies, is a part of the L4 series. This paper provides some insight into the developments of L4 and seL4 in particular.

https://dl.acm.org/citation.cfm?id=2893177

how is it possible to be unhackable? You might have to be a squad of 14 Terry A. Davis's and 53 Eliot aldersons, to find a backdoor, but they would have still found a backdoor. Anything can be hacked, and it being open source only helps