>he's not running a mathematically proven-correct, secure microkernelrofl. You're fucking shit.https://sel4.systems/https://research.csiro.au/tsblog/sel4-raspberry-pi-3/

Name
Email
Subject
Comment *
File	Select/drop/paste files here
Password	(Randomized for file and post deletion; you may also set your own.)
* = required field	[▶ Show post options & limits] Confused? See the FAQ.

Flag
Oekaki	Show oekaki applet (replaces files and can be used instead)
Options	Do not bump (you can also write sage in the email field) Spoiler images (this replaces the thumbnails of your images with question marks)
Allowed file types:jpg, jpeg, gif, png, webm, mp4, pdf Max filesize is 16 MB. Max image dimensions are 15000 x 15000. You may upload 3 per post.

[–]

▶Anonymous 05/04/18 (Fri) 05:29:23 No.908975>>908982 >>909019 >>910127 >>910132 >>910167 >>910386 [Watch Thread][Show All Posts]

>he's not running a mathematically proven-correct, secure microkernel

rofl. You're fucking shit.

https://sel4.systems/

https://research.csiro.au/tsblog/sel4-raspberry-pi-3/

▶Anonymous 05/04/18 (Fri) 05:36:40 No.908977

Are you?

▶Anonymous 05/04/18 (Fri) 05:37:46 No.908979>>908982 >>908983 >>910300

mathematically proven-ness is only applicable to small programs, you can't apply it to big piece of software such a kernel

▶cuteposter 05/04/18 (Fri) 05:41:22 No.908982

File (hide): d15ec4fbf16859a⋯.jpg (311.74 KB, 600x600, 1:1, smle-anime-animal-girls-19….jpg) (h) (u)

>>908975 (OP)

I WANT IT! OwO

It just needs a userland, which it seems will be provided by Genode OS framework.

>>908979

Good thing it's a microkernel uwu

▶Anonymous 05/04/18 (Fri) 05:41:37 No.908983

File (hide): bd33d2660c3fb13⋯.jpg (133.97 KB, 800x800, 1:1, 12389231.jpg) (h) (u)

>>908979

Are you retard?

▶Scheme Is Life!!sywAiVACmM 05/04/18 (Fri) 07:31:26 No.909019

>>908975 (OP)

Not enough Fashy imagery.

▶Anonymous 05/04/18 (Fri) 18:56:28 No.909292>>910102 >>910146 >>910151 >>910458

And what does it actually accomplish except satisfying your autism?

▶Anonymous 05/06/18 (Sun) 01:21:06 No.910102>>910129 >>910877

>>909292

Maybe if you had a fucking education in computer science or mathematics or computer engineering OR SOME FUCKING KNOWLEDGE REQUIRED TO ACTUALLY UNDERSTAND INTELLIGENT PROGRAM DEVELOPMENT, you would have an idea.

Go look up why mathematically proving code is a good thing, you fucking retard.

▶Anonymous 05/06/18 (Sun) 02:53:19 No.910127

>>908975 (OP)

>rofl. You're fucking shit.

Likewise. You certainly didn't make this post from a system running seL4 as the only kernel.

▶Anonymous 05/06/18 (Sun) 03:07:05 No.910129

>>910102

>"education in """"""" computer science """"""""" "

haha

▶Anonymous 05/06/18 (Sun) 03:17:54 No.910132>>910151 >>910167 >>910338

File (hide): b3caf62ed52c9ec⋯.jpg (18.15 KB, 367x380, 367:380, Absolutely_disgusting.jpg) (h) (u)

>>908975 (OP)

>Antifa-inspired RMS meme

Please do not do this

▶cuteposter 05/06/18 (Sun) 04:30:49 No.910146>>910462

File (hide): 807d64d38e57ba4⋯.png (239.29 KB, 500x520, 25:26, anime-boy-cute-penguin-nag….png) (h) (u)

>>909292

OwO whats this?

https://sel4.systems/Info/Docs/GD-NICTA-whitepaper.pdf

Theres another one here. link is to the page to pay although im sure theres ways around it if u dont want to. this one goes way more in detail and a lot of it is waaay over my head but hopefully it helps! ^_^

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

▶Anonymous 05/06/18 (Sun) 04:38:33 No.910151>>910169 >>910378

>>909292

Because it has the benefits of actually knowing what your system is doing, just like open-source, except it goes beyond just claims about what the code is doing and instead ACTUALLY MATHEMATICALLY PROVES that it does what it says it does.

This is so important for the future of security.

>>910132

>GNU totenkopf

>le antifa meme

▶Anonymous 05/06/18 (Sun) 05:40:58 No.910167

>>908975 (OP)

Don't listen to >>910132

Please do this

But make it nazbol.

▶Anonymous 05/06/18 (Sun) 05:43:43 No.910169>>910378

File (hide): cc12cb82066dd26⋯.jpg (1.01 MB, 2430x2672, 1215:1336, 7cbd262ecadfda7d1e3b7aa169….jpg) (h) (u)

>>910151

>oc symbol is antifa

>copted by the fash

>fash calls it theirs

The right can't meme

▶Anonymous 05/06/18 (Sun) 07:32:37 No.910212

While proven correct for what, one architecture, it is not proven secure.

▶Anonymous 05/06/18 (Sun) 10:42:05 No.910276

I don't run sel4 because camkes is shit and i'm too busy with my shitty projects to improve sel4 ecosystem.

▶Anonymous 05/06/18 (Sun) 11:24:01 No.910300

>>908979

>What is the B-method?

▶Anonymous 05/06/18 (Sun) 13:07:38 No.910338

>>910132

> implying antifa made the original meme

kek

▶Scheme Is Life!!sywAiVACmM 05/06/18 (Sun) 14:25:29 No.910378

>>910169

>>910151

It is called "shitting up your memes"

▶Anonymous 05/06/18 (Sun) 14:34:54 No.910386>>910401

>>908975 (OP)

>he runs a web browser with more lines of code than Windows 8 on his secure kernel and thinks he's secure

rofl. You're fucking shit.

▶Anonymous 05/06/18 (Sun) 15:49:24 No.910401

>>910386

>Have formally verified separation kernel

>browser misbehaves

>doesn't have access to other parts of the system.

▶Anonymous 05/06/18 (Sun) 17:06:32 No.910427

theres no proof for x86

▶Anonymous 05/06/18 (Sun) 18:17:08 No.910455>>910542 >>910576

File (hide): d072da268555279⋯.mp4 (652.34 KB, 1280x720, 16:9, awoogirl_local grill goes ….mp4) (h) (u) [play once] [loop]

>The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is available as open source.

I came.

>seL4 on the Raspberry Pi 3

then I came again.

▶Anonymous 05/06/18 (Sun) 18:20:57 No.910458

File (hide): f85ae451a6f1448⋯.png (207.88 KB, 500x700, 5:7, OReillyCIAniggersTerryDavi….png) (h) (u)