Return Styles: Pseud0ch, Terminal, Valhalla, NES, Geocities, Blue Moon. Entire thread

seL4 formally verified microkernel

Name: Anonymous 2016-06-23 3:45

https://sel4.systems/

This is the kernel that flies the X-37 Orbital Test Vehicle. Why aren't you using it in your embedded programming?

Anyway, this got me thinking about formal verification. Is it overrated crap to suck out more research grant money, or is it worthwhile to learn and apply?

Does it make unit-testing look like something retarded drooling code-monkeys do?

It seems difficult to use in the real world. Can it be made simpler? What if everything was written with formal proofs?

Are dynamically typed languages impossible to automatically verify?

Name: Anonymous 2016-06-23 4:01

Were you at the Coq fight last night?

Name: Anonymous 2016-06-23 6:35

seL4's implementation is formally (mathematically) proved correct (bug-free)
correct (bug-free)

top kek

Beware of bugs in the above code; I have only proved it correct, not tried it.

Name: Anonymous 2016-06-23 6:56

>>3
It's being used in real world military appliances. General Dynamics helped develop it.

Name: Anonymous 2016-06-23 7:08

>>4
sure thing. but mathematical correctness doesn't prove it's completely bug-free. it means that if the assumptions are true, the implementation adheres to the specification. this allows for bugs if:
* specification contains logic flaws
* specification does not consider some special cases
* assumptions are not true

Name: Anonymous 2016-06-23 7:31

>>5
Right, but surely it helps you overcome the needle in haystack problem with testing? Instead of testing all possible inputs, which may be impossible, it allows you to verify if your program is correct for an entire algebraic group of inputs.

Name: Anonymous 2016-06-23 7:44

>>6
oh, I agree that formal verification can be useful (although the way it is done now means it's usually more hassle than it's worth). it's just that it isn't a silver bullet that will magically make everything bug-free and secure because it still requires correct specification (a big thing - there are plenty of serious bugs made at the design stage, and they often impact security) and correct assumptions (also a big thing - people won't always use your software the way you imagine them using it).

Name: Anonymous 2016-06-23 16:49

They ignored a very critical bug report where they made use of undefined behaviour without reason.

Name: Anonymous 2016-06-23 17:43

Check em

Name: Anonymous 2016-06-24 0:47

>>7
just because it's not perfect doesn't mean it isn't better than everything else out there.
when you've proved that the implementation conforms to the spec down to the hardware level, all you have to do is prove that the spec is correct. and mathematicians have been doing formal proofs for 200 years, so that's not a mystery.
after that, the only thing you've got left to worry about is cosmic rays flipping bits.

Name: Anonymous 2016-06-24 19:44

The top agenda should be a formally proven browser and javascript engine. Of course, that would require a real standard to write to, not a moving target where one browser adds something so the others do it too, then it gets put in tutorials and referenced on StackOverflow to become the standard.

Name: Anonymous 2016-06-24 22:23

formally prove my anus

Name: Anonymous 2016-06-24 23:05

>>8
Link?

Name: Anonymous 2016-06-24 23:19

>>13
https://github.com/seL4/seL4/issues/2

Name: Anonymous 2016-06-24 23:31

Check em

Name: Anonymous 2016-06-25 0:52

>>8
This implies something pretty cool: we don't have to care whether the code violates the C standard or not. We can prove that it works anyway, even if it does. In reality, we are sticking to the standard very closely, though.
That's pretty cool

Name: Anonymous 2016-06-25 16:48

Why aren't systems like PVS, ACL2, Twelf, and TLA+ as popular as Coq and Isabelle?

>>11
http://goto.ucsd.edu/quark/

Name: Anonymous 2016-06-25 17:08

>>17
Aren't PVS and ACL2 the most popular provers for hardware verification?

Name: Anonymous 2016-06-26 14:45

>>18
Verify these dubs

Name: Anonymous 2016-06-27 9:09

>>10
you're forgetting assumptions. IIRC seL4 assumes no side-channel crypto attacks which is very generous

Name: Anonymous 2016-06-27 15:30

>>17
Because they all sound like shit, while coq sounds like cock (the bird) and Isabelle is a glorious name.

Name: Anonymous 2016-06-27 15:36

██████████ ████ ████ ███████████ ██████████ ████ ████
██████████ ████ ████ ███████████ ██████████ ████ ████
██████████ ████ ████ ████ ██████████ ████ ████
████ ████ ████ ████ ████ ████ ████
████ ██████████████ ████ ████ ████ ████
████ ██████████████ ███████████ ████ █████████
████ ██████████████ ███████████ ████ █████████
████ ████ ████ ████ ████ ██████████
████ ████ ████ ████ ████ ████ █████
██████████ ████ ████ ████ ██████████ ████ ████
██████████ ████ ████ ███████████ ██████████ ████ ████
██████████ ████ ████ ███████████ ██████████ ████ ████

███████████ ████ ████ ███████████ ██████ ██████
███████████ ████ ████ ███████████ ███████ ███████
████ ████ ████ ████ ████████ ████████
████ ████ ████ ████ ████ ████ ████ ████
████ ██████████████ ████ ████ ████████ ████
████ ██████████████ ███████████ ████ ██████ ████
████ ██████████████ ███████████ ████ ████ ████
████ ████ ████ ████ ████ ████
████ ████ ████ ████ ████ ████
████ ████ ████ ████ ████ ████
████ ████ ████ ███████████ ████ ████
████ ████ ████ ███████████ ████ ████

Name: Anonymous 2016-06-28 15:25

>>22
Dubs checker: v0.13 Input:22 Result: OK
____________
< Well done! >
------------
\ ^__^
\ (oo)\_______
(__)\ )\/\
||----w |
|| ||
Newer Posts
Don't change these.
Name: Email:
Entire Thread Thread List
All trademarks and copyrights on this site are owned by their respective parties. All comments and posts are the responsibility of their own posters.
- Tinychan + 2ch Mode + RSS -