[ / / / / / / / / / / / / / ] [ dir / baphomet / caco / choroy / christ / dbv / dempart / gfl / leandro ]

/tech/ - Technology

Winner of the 75nd Attention-Hungry Games
/caco/ - Azarath Metrion Zinthos

March 2019 - 8chan Transparency Report
Comment *
Verification *
Password (Randomized for file and post deletion; you may also set your own.)
* = required field[▶ Show post options & limits]
Confused? See the FAQ.
Show oekaki applet
(replaces files and can be used instead)

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.

File: ece9a83f8686fee⋯.png (145.71 KB, 1164x869, 1164:869, ClipboardImage.png)

File: 476655bb65f6593⋯.pdf (5.5 MB, SFO17-417-SEL4.pdf)


We need something better than all the Win/Mac/Linux shitware we have now. Software nowadays is unmaintainable and bloated as hell. The answer is a secure microkernel OS with formal verification and a clean codebase with minimalism and isolation in mind.


File: 286147ee126a2f9⋯.png (248.08 KB, 1123x751, 1123:751, ClipboardImage.png)

File: 373d8b3c234b41f⋯.png (219.05 KB, 1157x761, 1157:761, ClipboardImage.png)

At this point, pretty much everything can be hacked. Our cars can be hacked (which will become even more serious with the self-driving ones). Everything is connected and sending signals. The IoT is coming.

This wouldn't be such a problem if the software was actually designed properly


File: f03f6631e515da6⋯.png (146.77 KB, 1140x747, 380:249, ClipboardImage.png)

File: 9f1353d36dae557⋯.png (213.65 KB, 1210x819, 1210:819, ClipboardImage.png)

It's impossible to truly know how many bugs are in our code, but a general rule of thumb is that for every thousand lines, there are about one to five bugs. That sounds reasonable... until you realize how fucking massive codebases are. The Linux kernel is in the tens of millions now, and Bluetooth alone is hundreds of thousands. As system complexity goes up, the security goes down.

It's not just macroshit. It's Loonix too.


File: 958a6bf30eb00f7⋯.png (140.21 KB, 1177x724, 1177:724, ClipboardImage.png)

File: 36a6374cb6059bc⋯.png (164.94 KB, 1240x806, 20:13, ClipboardImage.png)

Yeah we could patch stuff, and we do. Oh we certainly do, but with our massive codebases, there are massive amounts of bugs. Eventually a vulnerability comes out, which prompts devs to actually do something about one, so they patch it. Yay, we removed one bug! Except in the process of patching, or in the process of continuing to maintain the program, we just introduced another bug. And the cycle continues...

Sure we could use firewalls, but that doesn't treat the problem at the root. It only mitigates our issues. Actually it barely does that, because our firewalls also run on big vulnerable operating systems with millions of lines of code, often the same ones we use on our normal systems.


File: a2f3e71fd5f3130⋯.png (149.72 KB, 1212x800, 303:200, ClipboardImage.png)

File: 7c987f500d202bd⋯.png (161.93 KB, 1186x773, 1186:773, ClipboardImage.png)

File: 65d09c392d78655⋯.png (137.87 KB, 1162x746, 581:373, ClipboardImage.png)

And no, the AI and machine learning memes won't help. They're the same shit as firewalls. They run on a broken foundation, and once again don't actually treat the core of what's wrong.

We need an operating system running on a trustworthy kernel, one that isolates processes based on whether they are critical and trusted or not. What is malware? What is malicious activity? A common definition is a program that does something that the user does not know it will do, does not expect, is not documented or specified. Therefore, a trustworthy program is one the conforms exactly to its specification, does things in a timely manner, and ensures that things will be executed securely. We need to think of this the same way we think of network security. There's the ideal of zero trust. We don't allow traffic in unless it is confirmed to be safe. Whitelist instead of Blacklist. In the same way, a system must be considered untrustworthy unless proven otherwise.


Important topic OP. We can probably look at hard realtime OSs and software used in mil aerospace for good ideas.




File: 542e35da6a10320⋯.png (188.35 KB, 1186x797, 1186:797, ClipboardImage.png)

Enter, SeL4, the provably secure operating system kernel. This little fucker is only 10k lines of C and ASM. This gives it a really small attack surface and means it can be verified FULLY. Now I know what you're thinking. "Oh but it's a MICROKERNEL! They're so slow they're a failed academic meme just look at muh mach!"

Mach was like four decades ago at this point. Microkernels have progressed a lot since then. In fact, they can be really, really freaking fast.

This one in particular also makes use of capability-based security. It may be small, but it doesn't take shit from anyone. Non-kernel code can only access stuff if it's explicitly allowed. If not, tough luck, CIAniggers.

There can be unprivileged code, but it certainly shouldn't be anywhere near the kernelspace. That's the privileged core of the operating system, and we need to keep it secure.


File: 036978badd508a6⋯.png (248.71 KB, 1196x798, 598:399, ClipboardImage.png)

And to hammer that point home about the developments, see this lovely chart of the microkernel innovations stemming from the original L3 and L4. This stems all the way back from 1993, and has gone in so many interesting directions. From ports to MIPS and Alpha, to inspirations off into Fiasco and Pistacho, the latter of which has variants seen in Apple and Qualcomm products. seL4 is just the latest and greatest in this line.



Whose done the full audit on it? I literally only trust a crowd-sourced effort tbh. Web of trust and all that.

> "“Oh, the jobs people work at! Out west near Hawtch-Hawtch there's a Hawtch-Hawtcher bee watcher, his job is to watch. Is to keep both his eyes on the lazy town bee, a bee that is watched will work harder you see. So he watched and he watched, but in spite of his watch that bee didn't work any harder not mawtch. So then somebody said "Our old bee-watching man just isn't bee watching as hard as he can, he ought to be watched by another Hawtch-Hawtcher! The thing that we need is a bee-watcher-watcher!". Well, the bee-watcher-watcher watched the bee-watcher. He didn't watch well so another Hawtch-Hawtcher had to come in as a watch-watcher-watcher! And now all the Hawtchers who live in Hawtch-Hawtch are watching on watch watcher watchering watch, watch watching the watcher who's watching that bee. You're not a Hawtch-Watcher you're lucky you see!”

>t. Dr. Seuss, Did I Ever Tell You How Lucky You Are?



It has proofs that verify its correctness.



>verified FULLY.

where "fully" means "as far as the model we are using allows it."

Before side channels for example became a thing no one was thinking about them in their proofs. You cannot protect yourself against the unknown unknowns.


File: ba9bfd4b1da17e7⋯.png (287.57 KB, 1151x787, 1151:787, ClipboardImage.png)

File: edb95c15ee609bc⋯.png (156.29 KB, 1153x789, 1153:789, ClipboardImage.png)

The security of such a kernel can be proven at all levels, even down to the fundamentals of security in terms of Confidentiality, Integrity, and Availability. It goes down to an abstract specification model (haskell I believe), then into its standard C/ASM implementation, with functional correctness checks done to ensure that it conforms. SeL4 even goes a step deeper and confirms the correctness of the translation from C to binary: that the compilation was done correctly and didn't create any inconsistencies.

As of now, this model does not account for system initialization, low-level MMU model, caches, multicore, and covert timing channels, but it does make the following provably impossible.

>buffer overflows

>null-pointer dereference

>code injections

>memory leaks

>kernel crashes

>undefined behavior

>privilege escalation

That's a lot more than you can say for other kernels. Others of this type tend to not only be slower, but offer no guarantees of functional correctness or translation correctness, no isolation of trusted/untrusted processes, only estimates for worst-case latency bounds, no guarantees of storage channel freedom, possibly a high timing channel prevention overhead, and limited mixed-criticality support


File: a762193aec2156c⋯.png (85.24 KB, 1154x779, 1154:779, ClipboardImage.png)

File: 7afb58a35663225⋯.png (183.05 KB, 1150x775, 46:31, ClipboardImage.png)

Ya know, this sort of system would make a great hypervisor as well. It could run virtual machines and make IPC calls with them. With seL4's isolation, it would be secure as well, as it would keep the bloated, legacy code away from newer, more safely designed code.


File: c725394569dae2a⋯.png (691.13 KB, 1153x797, 1153:797, ClipboardImage.png)

An interesting point that an anon made here was about the military >>1041243

That's because this stuff is actually already being used and researched by the Department of Defense's agency DARPA, as part of their High Assurance Military Systems Program. They can both retrofit their existing systems with this newer, more secure platform, such as with Boeing unmanned Little Birds or the US Army's autonomous trucks, as well as develop new technology such as drones and intelligent ground vehicle bots (which are kinda cute tbqhfam)



>Before side channels for example became a thing no one was thinking about them in their proofs

Do remember that you don't prove things secure, but rather prove invariants hold. For example, we could prove that there are no buffer overflows or that superuser only functions can not be run by regular users.


File: d279cf37b0b2e3e⋯.png (127.77 KB, 1197x751, 1197:751, ClipboardImage.png)

File: 056bc1d2c0b57a6⋯.png (151.43 KB, 1167x799, 1167:799, ClipboardImage.png)

File: 45ef3f4f11ebe6c⋯.png (132.26 KB, 1171x794, 1171:794, ClipboardImage.png)

The examples section is where I'm a bit too brainlet to explain, but there is quite an interesting diagram here at third pic related showing how this virtualization idea from earlier plays into the design of a HACMS UAV. Certain components that haven't been implemented in a trusted manner such as camera and Wi-Fi are contained in a separated Linux instance, while others such as crypto implementation and drivers for radio and controller area network are run natively directly on seL4.


File: d2f78b4d79eded8⋯.png (188.18 KB, 1171x795, 1171:795, ClipboardImage.png)

File: cdd9040d5fdd197⋯.png (135.47 KB, 1166x798, 583:399, ClipboardImage.png)

File: 25db776c212d580⋯.png (310.42 KB, 1148x732, 287:183, ClipboardImage.png)

Putting it all together. This is true military-grade security, which is being worked on in the US, UK, Australia, and Canada.


File: d4a47657b1650f5⋯.png (160.99 KB, 1152x808, 144:101, ClipboardImage.png)

Contribution to seL4


It doesn't matter how secure OS will you do, because your (((Intel))) CPU has another CPU inside it with botnet closed operating system, that spies on you and sends your keystrokes to Israel



So did WPA2. Then they read the spec and realized it was brain dead retarded. Formal proofs only prove that the spec is implemented correctly. Issue is that the formal spec is probably almost as difficult to read as any source code would be.



>Enter, SeL4, the provably secure operating system kernel. This little fucker is only 10k lines of C and ASM.

if it's made in C and ASM, then this shit cannot be safe


File: bd6b31e618e26fc⋯.png (331.12 KB, 955x576, 955:576, ClipboardImage.png)

File: baa0c2256959135⋯.png (124.99 KB, 959x402, 959:402, ClipboardImage.png)


Sauce code here


An operating system that can utilize seL4 and other microkernels of this type.


A look at its architecture


Road map. This year they plan to work on making it usable for common use cases.


They already accomplished one of their goals (OpenJDK support).




Not for long. SeL4 supports ARM, and ARM becoming more powerful and accessible. Applel has been playing around with the idea of moving macs to it, there's server systems running on ThunderX chips, and System76 is working on ARM workstations and laptops as we speak.



"""military grade"""


Also tagged processes and threads - you could set tags on processes and threads and they can only request syscalls/call functions/load libraries which are tagged the same tags a process/thread is tagged. Any other syscall/function call/library load either silently fails or errors. Only user can set tags. This will surely be a bit more secure since a calculator app wouldn't have access to FS, low-level graphics, or encryption but it will have access to mathematic functions and high-level UI API.



a smart lightbulb which thru an encrypted ZigBee protocol? connects to bridge which then using an encrypted VPN connects to company's server/your home server and allows you to control the lightbulb from your office using REST/GraphQL/whatever shit



You can defuse the Managment Engine thing by setting a HAP bit and removing the ME firmware from your BIOS/replacing it with a program which starts up a simple HTTP server which outputs a picture of a cat on every HTTP request



>This will surely be a bit more secure since a calculator app wouldn't have access to FS, low-level graphics, or encryption but it will have access to mathematic functions and high-level UI API.

This. It's a lot like how capability-based security is commonly described.


>Capabilities achieve their objective of improving system security by being used in place of forgeable references. A forgeable reference (for example, a path name) identifies an object, but does not specify which access rights are appropriate for that object and the user program which holds that reference. Consequently, any attempt to access the referenced object must be validated by the operating system, based on the ambient authority of the requesting program, typically via the use of an access control list (ACL). Instead, in a system with capabilities, the mere fact that a user program possesses that capability entitles it to use the referenced object in accordance with the rights that are specified by that capability. In theory, a system with capabilities removes the need for any access control list or similar mechanism by giving all entities all and only the capabilities they will actually need.


When I originally told you "All is botnet" I had already seen the future this is to come.



Fags like OP continue to not use real time operating systems properly, so I can't take them seriously.


You are wasting your time with a RTOS if you do not understand the mathematics involved with the proof verification that governs it. Your CS degree is worthless here.



Arm has the same problem, if not, worse.


Thanks for all the unreadable thumbnails



Protip: if you click them you get a readable image of the slide!



>Open source is justice!



I find that hard to believe. ARM is not the retarded duopoly that we have with Intel and AMD. There's a lot of different vendors that can make ARM chips.

And, failing that, there's always RISC-V, which seL4 also supports or at least plans to support, as does Genode.



Ok, I'll make the logo


File: 48caecd0d6148c9⋯.png (6 KB, 600x300, 2:1, seL4-logo.png)

File: 4f5918435a866ab⋯.png (82.5 KB, 684x137, 684:137, genode.png)


Someone beat ya to it.



Is it normal for my nipple to get hard when I poop? I'm a hetero male, fwiw



Yeah it's fine, breh


>formal verification

Do we aim to write this in a functional language LMAO?


File: d7bcd343e962208⋯.jpg (20.93 KB, 600x576, 25:24, Hold Up.jpg)


So what you're saying is that non-privileged components have absolutely no way whatsoever of accessing privileged components or using it in any way? This sounds like a huge bottleneck by default, and if they're even given a single chance to access privileged components by the kernel, then that opens up loads of potential breach points which defeats the whole purpose of the kernel. Unless I'm acting like a retard who has no idea what any of this means.



Slides look like Microsoft kernel engineering talks from 2015...

Windows 10 HAS a secure isolated microkernel for the critical stuff like random number generation.



Unironically yes. The specification was in Haskell from what I understand.


File: 1470374ea332f18⋯.jpg (92.42 KB, 609x295, 609:295, 2_14_microkernelArchitectu….jpg)


Yeah you are, but thats ok.

>Inter-process communication (IPC) is any mechanism which allows separate processes to communicate with each other, usually by sending messages. Shared memory is strictly speaking also an inter-process communication mechanism, but the abbreviation IPC usually only refers to message passing, and it is the latter that is particularly relevant to microkernels. IPC allows the operating system to be built from a number of small programs called servers, which are used by other programs on the system, invoked via IPC. Most or all support for peripheral hardware is handled in this fashion, with servers for device drivers, network protocol stacks, file systems, graphics, etc.

>In the context of security the minimality principle of microkernels is, some have argued, a direct consequence of the principle of least privilege, according to which all code should have only the privileges needed to provide required functionality. Minimality requires that a system's trusted computing base (TCB) should be kept minimal. As the kernel (the code that executes in the privileged mode of the hardware) has unvetted access to any data and can thus violate its integrity or confidentiality, the kernel is always part of the TCB. Minimizing it is natural in a security-driven design.



This. Forth on bare metal.

[Return][Go to top][Catalog][Nerve Center][Cancer][Post a Reply]
Delete Post [ ]
[ / / / / / / / / / / / / / ] [ dir / baphomet / caco / choroy / christ / dbv / dempart / gfl / leandro ]