/tech/ - Technology★

>>878163 (OP)

Daily reminder that formal verification only proves the relationship of a model to an implementation and that it is not proof that the model has anything to do with reality / accurately deals with threats.

it doesn't have any proofs for x86 you fucking shill fuck off. you've been posting this all day on g too.

>>878173

ARM is the future, anon.

https://www.qualcomm.com/products/qualcomm-centriq-2400-processor

https://www.cavium.com/product-thunderx2-arm-processors.html

>>878173

x86 is so fucking complicated if they could not possibly model it correctly. The "proof" would be meaningless.

>>878169

There was actually already a bug in one of the unverified parts that had to be fixed. It's still a good choice if you need it but if you post here you don't.

>>878307

>2015

>he still thinks serious business government and corporations have both super duper security requirements and the means to satisfy them

Is it webscale?

>>878163 (OP)

>mathematically-verified bug-free

wat

>>878556

https://wiki.sel4.systems/FrequentlyAskedQuestions

>Formal software verification is the activity of using mathematical proof to show that a piece of software satisfies specific properties.

>Unique about seL4 is its unprecedented degree of assurance, achieved through formal verification. Specifically, the ARM version of seL4 is the first (and still only) general-purpose OS kernel with a full code-level functional correctness proof, meaning a mathematical proof that the implementation (written in C) adheres to its specification. In short, the implementation is proved to be bug-free (see below). This also implies a number of other properties, such as freedom from buffer overflows, null pointer exceptions, use-after-free, etc.

>There is a further proof that the binary code which executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary.

>Furthermore, there are proofs that seL4's specification, if used properly, will enforce integrity and confidentiality, core security properties. Combined with the proofs mentioned above, these properties are guaranteed to be enforced not only by a model of the kernel (the specification) but the actual binary that executes on the hardware. Therefore, seL4 is the world's first (and still only) OS that is proved secure in a very strong sense.

>Finally, seL4 is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees.

>The new and exciting thing about seL4 is that is has a) strong properties such as functional correctness, integrity, and confidentiality, and b) has these properties formally verified directly to the code --- initially to C, now also to binary. In addition, the seL4 proofs are machine-checked, not just based on pen and paper.

>Previous verifications have either not completed their proofs, have targeted more shallow properties, such as the absence of undefined execution, or they have verified manually constructed models of the code instead of the code itself.

TL;DR: They mathematically verify that there's no buffer overflows, null pointer exceptions, etc, ensure that the binary is correctly compiled (immune to the theoretical Ken Thompson Hack), and are far more thorough with their verification process than any other general-purpose OS kernel.

>>878174

wrong. RISC-V is the future

>>878567

Good point.

but ARM is the immediate future

>>878567

>>878569

also, even if RISC-V does surpass ARM at some point, and seL4 does not get a port to it, Genode OS will still be important, as a set of drivers and utilities that can be used across multiple microkernels.

https://genode.org/documentation/components

Will Hurd use this now?

>>878578

I think I remember seeing something about them considering it, but seeing as how HURD moves at a snail's pace, who knows what they'll end up doing

>>878578

Nobody in the Hurd team is actively working on porting Hurd to L4. They've done evaluations in the past and decided they'd rather continue with Mach.

>>878592

HURD is a piece of nearly-abandoned trash at this point. I have no idea why anyone cares about it

>>878596

I love the potential of the Hurd. The flexibility of the Mach translator system is unparalleled to any system we have today. If your hardware is supported, then you can actually run Hurd today in the command line and with difficulty through Gnome 3. What they're doing at the moment is implementing a rump kernel* so that Hurd can finally get more drivers working than the ancient drivers that exist.

* http://rumpkernel.org/

>>878596

The HURD is never going to be released using Mach, much less anything else, but the paradigm of microkernel+dmd+guix is pretty awesome.

>>878600

GNU DMD has been renamed to GNU Shepherd.

>>878566

>(immune to the theoretical Ken Thompson Hack)

>The trap doors described in the report were patches to the binary object files of the system. The report suggested a countermeasure to such object code trap doors by having customers recompile the system from source, although the report also notes that this could play directly into the hands of the penetrator who has made changes in the source code. In fact, the AFDSC Multics contract specifically required that Honeywell deliver source code to the Pentagon to permit such recompilations. However, the report pointed out the possibility that a trap door in the PL/I compiler could install trap doors into the Multics operating system when modules were compiled and could maintain its own existence by recognizing when the PL/I compiler was compiling itself. This recognition was the basis several years later for the TCSEC Class A1 requirement for generation of new versions from source using a compiler maintained under strict configuration control. A recent story on CNET news [14] reports that the Chinese government has similar concerns about planted trap doors.

>This suggestion proved an inspiration to Ken Thompson who actually implemented the self-inserting compiler trap door into an early version of UNIX. Thompson described his trap door in his 1984 Turing Award paper [40], and attributed the idea to an “unknown Air Force document,” and he asked for a better citation. The document in question is in fact the Multics Security Evaluation report, and we gave a new copy of the report to Thompson after his paper was published. Thompson has corrected his citation in a reprint of the paper [39].

http://hack.org/mc/texts/classic-multics.pdf

>>878814

What a hack. The Unix Hater was right.

>>878599

Just begging for a Trump Kernel fork

>>878163 (OP)

If you haven't tried the new 2018.02 release of Genode it's actually really cool. There's almost complete hardware support for various Thinkpads, including a work-in-progress 3D driver for Intel iGPUs. The Genode package binaries themselves are identical across microkernels now, so once a driver works on NOVA or base-hw it'll work on seL4.

https://genode.org/documentation/release-notes/18.02

http://genode.org/documentation/articles/sculpt-ea

https://genode.org/about/road-map

>>878599

I think this makes a lot of sense. Everything used to be usable with less code. Drivers are more bloated now even though the hardware does a lot more work and could present a simpler interface to the computer.

http://www.fixup.fi/misc/usenix-login-2015/login_oct15_02_kantee.pdf

>As a result of added I/O device processing power, what else is obsolete in the software/hardware stack? One is tempted to argue that everything is obsolete. The whole hardware/software stack is bifurcated at a seemingly arbitrary position which made sense 30 years ago, but no longer. Your average modern I/O device has more computing power than most continents had 30 years ago. Pretending that it is the same dumb device that needs to be programmed by flipping registers with a sharpened toothpick results in sad programmers and, if not broken, at least suboptimal drivers. Does doing 802.11 really require 30k+ lines of driver code (including comments), 80k+ lines of generic 802.11 support, and a 1 MB firmware to be loaded onto the NIC? For comparison, the entire 4.3BSD kernel from 1986 including all device drivers, TCP/IP, the file system, system calls, and so forth is roughly 100k lines of code. How difficult can it be to join a network and send and receive packets? Could we make do with 1k lines of system-side code and 1.01 MB of firmware?

>The solution for hardware device drivers is to push the complexity where it belongs in 2015, not where it belonged in 1965. Some say they would not trust hardware vendors to get complex software right, and therefore the complexity should remain in software running on the CPU. As long as systems software authors cannot get software right either, there is no huge difference in correctness. It is true that having most of the logic in an operating system does carry an advantage due to open source systems software actually being open source. Everyone who wants to review and adjust the 100k+ lines of code along their open source OS storage stack can actually do so, at least provided they have some years of spare time. In contrast, when hardware vendors claim to support “open source,” the open source drivers communicate with an obfuscated representation of the hardware, sometimes through a standard interface such as SATA AHCI or HD audio, so in reality the drivers reveal little of what is going on in the hardware.

>>878566

you stupid neckbeard wannabes are so dense you think some type of backdoor has to be called a "Ken Thompson Hack" because you're too stupid to realize where backdoors can exist until some famous guy says explains it for you

>>878556

not sure whether

>hurr durr formal proofs don't work in practice. MUH PRACTICE!11

or

>i'm 12 and what is formal proofs

>>878599

Genode uses rump kernel versions of Linux, OpenBSD, and NetBSD for much of its driver support.

>>881290

The author forgets how staggeringly incompetent OEMs are, and fails to recognize the added ability for (((software differentiation))) of products. Keeping drivers on the main CPU is entirely worth it for kneecapping peripheral manufacturers' ability to do chinky/kikey bullshit alone.

>>878567

By the time RISC-V is matured, no normie will even want to own a general-purpose computing device anymore, they'll be perfectly happy with botnet terminal devices. Heck, those botnet terminal devices will come built-in with anything else anyway as part of the """internet or things""", so worrying about even that will be completely superfluous. Actual computing will be restricted to the military, gubmint, and biggest corporations who operate """cloud""".

>>878163 (OP)

>seL4

Has this anything at all to do with SELoonix (aka _NSAKEYLoonix)?

>>884467

No

Microkernels written in C aren't a solution. I wouldn't want to use seL4 because it doesn't improve the user's quality of life. On a Lisp machine, Go and scripting languages would do everything worse than the OS already does, so there's no point. On UNIX, Go and scripting languages are huge projects with a ton of code because the only common language is C and everything else has to be done from scratch. Besides making things a lot easier, Lisp machines improved the quality of languages too. Fortran and Pascal on Lisp machines had bignum integers and used the same arrays and functions as Lisp so you didn't need an FFI. The machine had bounds checking, so there were no buffer overflows, and you could change the code and data and continue whenever there was an error. Multics had that kind of debugging too.

   Try the case where the interpreter specified on the #!
   line is *itself* implemented by an interpreted
   script. Now if a reasonable person were implementing
   this, it would just work.  Recursion is a concept
   understood by most 18-year-old CS majors.  Apparently
   this notion escaped the notice of the BSD/SunOS guys,
   because on my Unix, one level is all you get.

You Just Don't Understand.  Writing Code To Run Inside
Kernels Is A Hard Problem.  (That's why we have
microkernels; so you can have programmers of average ability
writing system software and not necessarily crashing
everything when it breaks.)  You can't just allow unbounded
recursion inside the Kernel.  You might overflow your Kernel
stack which is of course set at some small wired in constant
in keeping with unix tradition (Simple!).  And of course, No
One Would Ever Want To Specify Another Shell Script In The
#! Line.

I have a machine named EXXON-VALDEZ on my desk.  This was
from when I nominally worked in fault tolerant computing; I
figured it would be good karma to name the machine after a
huge disaster as a precautionary measure.  (I'm quite
superstitious in strange ways.)  Now the hardware has been
replaced and I'm about to name the machine something else.
I'm thinking of the name MBUF.  I suppose it wouldn't be
such a big change; the machine would still be named after a
huge disaster...

>>884574

Lisp machines turned out to be such a catastrophic dead end that quarter century old quips from the Unix Haters' Handbook are still the most recent complaints they have, even if most of the problems expressed in ugh.pdf were fixed by GNU/Linux and the BSDs later.

>>878567

Keep dreaming denialist

>>878567

>believing in RISCV

No normie will ever using it

>>885239

Stop caring about what normalfags do. The only thing they are good at is ruining things that are actually good.

>>885280

Normalfags do what the corporations want them to, if that is RISCV in consumer produts so it shall be, almost all of them will not even know it.

>>885286

PC OEMs are already looking into RISCV for better microcontrollers and peripheral chips. Windows and ESXi keep them tied to x86 CPUs for the foreseeable future.

>>885239

They will never use arm laptops either, o wait chromebooks are a thing.

>>885451

>chromebooks are a thing

Are they?

Is anyone except for shitty public schools really using them?

>>885502

https://www.pcworld.com/article/3194946/computers/chromebook-shipments-surge-by-38-percent-cutting-into-windows-10-pcs.html

I know tons of rando normies that use chromebooks, most of them are college students.

>>885502

Chromebooks are actually one of the most secure laptops on the market. It's sad that from that secure device, they require you to run Botnet OS.

>>885346

Reminder that it's BSD-licensed so no freedoms whatsoever.

>>885809

It's funny that 20 years later, the threat of browsers reducing Windows to a poorly debugged set of device drivers was true... but then Linux existed with the ability to write or improve your own device drivers, so that got used as the base for ChromeOS instead.

>>884574

meme machine

>>885819

Atleast it has more freedom than GPL

>>885990

Ah yes, the freedom to restrict freedom. Reminder that your freedom ends where someone else's freedom starts.

>>886008

>Reminder that your freedom ends where someone else's freedom starts.

Which is why no one else has a right to source code

>>886072

freedom ain't free

the tree of liberty and freedom gotta be littered with the blood of Patriots

>>886074

If I have 10 apples, and I give you 1 apple, I have not infringed on any of your freedom.

>>886008

Huh strange, is that not like the gpl restricting my freedom to use a license of my choice?

>>886087

No, but it is using intellectual property laws to restrict the freedoms of others.

>>886095

>implying its ok for the GPL to restrict your freedom but its not ok for someone else to restrict your freedom.

Why are you so dense?

>>886096

>implying its ok for the GPL to restrict your freedom

It's not okay for the GPL to restrict your freedom

>>886095

for your own safety and the safety of others do not question vital licensing apparatus

>>886098

Why are you shilling it if its not ok? I have already stated how it restricts your freedom, and what I mentioned isn't the only way it does.

>>886109

> I have already stated how it restricts your freedom

Did you not read the fucking text

>It's not okay for the GPL to restrict your freedom

Its NOT okay that the GPL restricts your freedom

this thread is about seL4

>>886113

>cuck license

>>886112

I'm not sure I am following these replies the same way you are, but thats fine since the same conclusion was reached in the end.

>>886119

If I have 10 apples, and I give you 1 apple, I have not infringed on any of your freedom.

>>886121

If I give you one apple and tell you I'll sue you if you bake it into a pie, I have infringed on your freedom.

>>886124

Right so having that apple that you can now eat is somehow less free than not have an apple.

Lolberts? On my board? It's more likely than you think.

A simple-minded right-wing ideology ideally suited to those unable or unwilling to see past their own sociopathic self-regard.

>>886129

>It was not real communism

>>886129

>Lolbert

<Be careful though. Only a lolbert can call another lolbert “lolbert.”

How Owners Justify Their Power

Those who benefit from the current system where programs are property offer two arguments in support of their claims to own programs: the emotional argument and the economic argument.

The emotional argument goes like this: “I put my sweat, my heart, my soul into this program. It comes from me, it's mine!”

This argument does not require serious refutation. The feeling of attachment is one that programmers can cultivate when it suits them; it is not inevitable. Consider, for example, how willingly the same programmers usually sign over all rights to a large corporation for a salary; the emotional attachment mysteriously vanishes. By contrast, consider the great artists and artisans of medieval times, who didn't even sign their names to their work. To them, the name of the artist was not important. What mattered was that the work was done---and the purpose it would serve. This view prevailed for hundreds of years.

The economic argument goes like this: “I want to get rich (usually described inaccurately as ‘making a living’), and if you don't allow me to get rich by programming, then I won't program. Everyone else is like me, so nobody will ever program. And then you'll be stuck with no programs at all!” This threat is usually veiled as friendly advice from the wise.

I'll explain later why this threat is a bluff. First I want to address an implicit assumption that is more visible in another formulation of the argument.

This formulation starts by comparing the social utility of a proprietary program with that of no program, and then concludes that proprietary software development is, on the whole, beneficial, and should be encouraged. The fallacy here is in comparing only two outcomes---proprietary software versus no software—and assuming there are no other possibilities.

Given a system of software copyright, software development is usually linked with the existence of an owner who controls the software's use. As long as this linkage exists, we are often faced with the choice of proprietary software or none. However, this linkage is not inherent or inevitable; it is a consequence of the specific social/legal policy decision that we are questioning: the decision to have owners. To formulate the choice as between proprietary software versus no software is begging the question.

https://www.gnu.org/philosophy/shouldbefree.en.html

>>886137

Developers should have no intellectual property rights. Which is why GPL is immoral. If a developer only wants to give away a binary though, you have no right to demand anything else from them.

>>886139

In an ideal world I would not care, because users would reject proprietary software so he can give out all the binaries he wants, nobody would use them. However in reality I want it to be as inconvenient as possible, because users are ignorant and the greedy developers know this and actively subvert the Free Software movement with Open Source (TM) to keep them that way in order to enrich themselves from the resulting power asymnetry.

>>886068

Genode isn't ready for anyone who's not familiar with the source code and build process yet. Wait for the August or November release.

>>886144

>because users are ignorant

Or they don't actually care if they are tracked because in almost every other way the software is superior

>>878592

I expect it is stallmans faultHis lunacy makes

the others want to overthrow the Hurd Reich

Genode has a Quake package now.

>>886139

I personally believe distributing binaries is immoral. You are giving someone else an obfuscated mess that humans can not understand.

it has no proofs for x86

google botnet garbage is the future?

>>886230

>You are giving someone else an obfuscated mess that humans can not understand.

I don't know how my car works, still glad to have it. Between a car I cant understand and no car I am more free with the car.

>>886237

The metaphor would be if your car did not come with a owner's / repair manual.

>>886240

All these metaphors are just meant to distract you from what matters. They are all wrong, cars are not artificially obfuscated and you could not build your own car from the materials and instruction, while everyone can compile the binary from the source on their pc. They are artificial restrictions to effectively continue owning something after you sold it, even multiple times. This is what libertarians want, the freedom to enslave you.

>>886232

fine by me. we need to get off x86 ASAP

>>886240

The point is exactly the same if it comes without them

>>886244

>the freedom to enslave you.

Yea giving you an apple with an agreement you won't bake it into a pie is enslaving you. Sure fucking thing.

>all these faggots screeching about seL4 being BSD licensed

>Genode is fucking AGPLv3

>Genode's in-house microkernel (also AGPLv3) will be capable of virtualization, SMP, and IOMMU on amd64 by the end of 2018 when seL4 still can't fucking do SMP

BSD cucks blown the fuck out yet again.

>>886274

but one is secure and the other is not (BSD wins again)

>>886265

Okay, I'll continue with your analogy. Let's say one of the belts in the engine snapped. If the car was like a binary, you would need to tell the manufacture of the car of the problem and then they consider shipping you out a new working engine. If the car was like the source, you could just replace the belt. Let's say you aren't knowledgeable about cars though. You can take your car to a mechanic to do it for you. You pay him for his time and you are off on your way.

With a binary, you are entirely dependent on the developers to make any changes to it. With source you can make changes that you see fit. If you do not know about the changes you can take them to a programmer to have him do it for you. You pay him for his time and you are off on your way.

>>886277

seL4 is just a microkernel. It doesn't do much of anything. Genode is actively secure despite being a much larger system, and works better on its own kernel or NOVA than on seL4.

>>886280

> and works better on its own kernel or NOVA

Which are not proven secure :^}

>>886279

>Let's say one of the belts in the engine snapped.

Well that fucking sucks, but the car was free so I now I am in the same position as before.

>>886281

Neither is seL4 on x86, or even on ARM with an MMU.

>>886294

>its not proven correct on all these other platforms so it does not count!

>>886296

The ONLY scenario that's verified is single core ARMv7 with the MMU turned off, so yes.

>>886300

Good enough for vi, and lynx

>>878174

Isn't ARM cucked?

>>893254

way less than x86, but still kinda cucked (not totally free like RISC-V)

>>878178

to be fair, it's reasonable to suspect they want to use shit that can't get assfucked by the CIAniggers of different countries.

>>884720

>Lisp machines turned out to be such a catastrophic dead end

Lisp machines didn't continue the race because the market was overflowed by 32bits CPU and nobody didn't see the reason in that time to have lisp machine which costed more.

>>893275

>costed

>>886137

I love putting nontrivial harmless bugs in my open source code for people like you.

The argument then becomes "Why should I fix my code for you unless you pay me for that service?"

Naturally, only those that are worthy of fixing the code themselves get to use it, as god intended. The rest better pay up.

Find a flaw with that you cancer.

And another thing, ownership is necessary for liability. If your code is used in a device that decides the fate of millions of people, you better be damn well prepared to accept liability if something goes wrong. Ownership is a double edged sword you idiot.

>>893702

>Ownership is a double edged sword you idiot.

Suuuuure I already see the guillotine used on the dude who made heartbleed.

>>893705

>he thinks people aren't paid to put bugs and backdoors in opensource projects by government intelligence

laughing girls.tif

>>893702

I've actually ran across a few projects VBAM, OSS, and another I forget the name of like this that I had to go and fix the code, being a trivial as fuck thing, to make it compile. There's one description for someone like you who intentionally leaves bugs for others, low quality workmanship and little pride in their work. It's the same type of thing pajeet does, leave bugs in the code or be so utterly incompetent to get re-hired at a company. It does keep idiots and normalfags out in a general sense, which does have merrit But in the same breath those same idiots and normalfags would never imagine how to compile software nor figure it out, hence crap workmanship.

>>886300

>turning the MMU off

Explain how this is possible.

>>885809

This is sad but true.

>>878571

Why should I contribute to genode when I can just take the seL4 framework of kernel API's, write a driver for my hardware periphials, and then port a c compiler to it? I would just have to make what is the equivelent of a stage1 gentoo install at that point and account for things like API's changes in the porting proccess.

>>893708

When you're work with ones and zeros, eventually you come to realize that you're merely working on top of someone else's platforms and ideals, which is filled with all their flaws and nuances. I have more pride in things I make myself that I can physically touch and operate.

>>893708

Are you seriously asking why shouldn't you contribute to an OS when you could write your oen, leaving only minimal parts of the kernel?

No, you know what? You are right, you shouldn't. Now go write several device drivers, rape a compiler and write the whole userland all alone. Show us what you are capable of, I will wait.

>>893723

He's living the dream and you have the audacity to insult him? For shame anon.

>>878169

>CY+4

>NOT coding to a model

https://www.fastcompany.com/28121/they-write-right-stuff

>>878169

And its probably vulnerable to cache side-band attacks because everyone's model of a cache has no side effects.

>>878323

seL4 is for drones, not high security.

>>881331

what's it like living in a social vacuum?