Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Fuchsia: a new operating system

lwn.net

Post reply on HN
Print view View original

271–280 of 324 posts

Re: Fuchsia: a new operating system

#271

Post by nickpsecurity »

qznc wrote: post #229
nickpsecurity wrote: post #173

Earlier quoted context omitted.

I think author meant L4 kernels were performance tuned for 20 years to be the fastest. Then, one using applying such lessons was mathematically verified for correctness down to assembly. It's proprietary and open-source depending on what your end product will be. They'd probably even add features to it for a Google-specific version that leveraged as many proven compinents as possible.

SeL4 is still working on multithreading. It is probably not good enough for a user interfacing OS yet.

That's true in its current state. Remember, though, that they're working on multithreading in a way that ties into their proof from high-level spec down to the code down to the assembly. Googles people are just putting together a kernel with review & testing. They could take seL4, modify it for concurrency, check it with concurrency-related tooling, and still get quite a bit of assurance from original work. Proof no longer applies but most things it applied to haven't changed. And model-checkers for concurrency are among easiest tools to use in formal verification w/ TLA+ getting adoption even by mainstream companies.

Re: Fuchsia: a new operating system

#272

Post by nickpsecurity »

pjmlp wrote: post #218
nickpsecurity wrote: post #170

Earlier quoted context omitted.

How about Muen separation kernel in SPARK Ada with automated prover eliminating many classes of undefined behavior? Or C with tools like Frama-C and Astree Analyzer (like SPARK for C)? C++ can't reach the safety of its competition due to more complexity and less tooling.

To be fair, if Frama-C is an option, as someone on the C++ side of the fence (C vs C++) I would advocate High Integrity C++ is also an option. :) http://www.ldra.com/en/software-quality-test-tools/group/by-...

I thought about it. The reason I left it off is a lack of static analysis, automatic generation of tests, certified compilers, etc. There's tons of FOSS and commercial vendors for doing such things in C with quite a bit for Ada. Whereas, I could find only one or two products for C++ that seemed like it would be really helpful as opposed to just kind of. So, I pivoted my recommendations to go with languages that have huge, tooling ecosystems in academic R&D and commercial. You can certainly use it but might get less value in long term.

Embedded, real-time Java could also be on the list since Java ecosystem has a verification tool for about everything. CompSci loves Java for some reason (probably mandated classes). Yet, verifiable C and SPARK are closer to the metal than embedded Java plus no Oracle risk. So, left off Java as well.

Re: Fuchsia: a new operating system

#273

Post by bonzini »

pjmlp wrote: post #222
MichaelMoser123 wrote: post #185

Lots of interest in Microkernels since everyone got tired of kernel vulnerabilities. So who won the Tanenbaum–Torvalds debate? It is too soon to say (Zhou Enlai said that of the French revolution - almost 200 years after the fact) https://en.wikipedia.org/wiki/Tanenbaum%E2%80%93Torvalds_deb... The article says that the focus is on 'PCs, tablets, and high-end phones'. Wouldn't a more secure OS be relevant to server en…

Given the amount of shipped embedded systems and the hybrid designs from OS X and Windows, I would say Tanenbaum won. The majority of embedded OSes have a microkernel design. Also Windows and OS X have a kind of hybrid design, even if not a proper mikrokernel. On Windows case,there are now a sandboxed kernel and drivers. https://channel9.msdn.com/events/Ignite/2016/BRK4010 https://channel9.msdn.com/Blogs/windowsserve…

Even with new features like Device Guard, Windows is all but a microkernel; parts of the GUI high-level primitives (like fonts) are in WIN32K.SYS. Even OS X moved a lot of drivers to kernel space, it's not a pure microkernel design like the Hurd.

If anything, the closest thing to a microkernel that is in wide use is Xen, or Hyper-V.

Re: Fuchsia: a new operating system

#274

Post by nickpsecurity »

protomyth wrote: post #107
puzzle wrote: post #66

Earlier quoted context omitted.

The future? The System/38 (aka AS/400 aka iSeries aka System i) had capabilities from the beginning, almost 40 years ago.

I sometimes wonder if addition to a Ethics class, Computer Science students need to take a Computer Archaeology class. It might not be a bad thing to bring up a lot of the concepts that aren't in the main stream anymore that have been tried.

I definitely support that. Many tips I give to people for their projects came straight out of 1960's-1980's CompSci or industrial work. It has been a ridiculous amount of effort finding all of it, though. So many silos. It needs integrated on a per topic basis, cleaned up, an executive summary, and references available for follow-up. Preferably with FOSS tools if it's an analytical method, language, etc.

Then, people might quite reinventing the wheel or missing obvious things as much as they do now.

Re: Fuchsia: a new operating system

#275

Post by paulddraper »

deno wrote: post #75
jjuel wrote: post #59

Earlier quoted context omitted.

Not often someone says lean and VS Code in the same statement.

It’s not very fast, but it’s surprisingly easy on the resources, especially memory. Compare using VS Code w/ Typescript Language Service to any type of dev stack that includes the word “Scala.”

Scala with Emacs + Ensime

Re: Fuchsia: a new operating system

#276

Post by throwayedidqo »

gkya wrote: post #250
throwayedidqo wrote: post #220

Fuchsia sounds awesome. Allowing user space processes to do more of their own work frees up the kernel from providing standardized interfaces to hardware. This makes it significantly easier to build a closed platform with unbreakable barriers between processes, and this is a great thing in terms of security and fine grained access controls for each process. Individual process isolation is extremely important for most…

This is a complete misunderstanding/misrepresentation of what a microkernel is. Even GNU is developing their own microkernel, the HURD.

I may be overly paranoid, but the majority of what Fuscia is trying to accomplish is extremely bad for open platforms.

The outcome of moving drivers to user space will be proliferation of binary blobs and black box drivers. If you think binary GPU drivers are bad now, imagine an "open source" OS where every single driver is a binary blob. It will become impossible to run Fuscia devices on any other operating system because you have no drivers, sealing off the Android platform permanently.

Re: Fuchsia: a new operating system

#277

Post by paulddraper »

andrewflnr wrote: post #230
CalChris wrote: post #90

I've been waiting for this to be released. I suppose everyone has been. Capabilities . Like fine grain locks, these are very powerful and very hard to get right. That's the lesson from Hydra, the 432, .... No, it's not a hard mechanism for the microkernel to get right; it's a hard policy for the application programmer to get right. However, that's probably more of an opportunity rather than meant as a criticism. Our…

Why do you want to implement something small with something that is large? Consider the size and amount of equipment involved in making watches. Or microchips, for that matter.

Do you carry that watch-making equipment on your wrist along with your watch?

Re: Fuchsia: a new operating system

#278

Post by nickpsecurity »

MichaelMoser123 wrote: post #185

Lots of interest in Microkernels since everyone got tired of kernel vulnerabilities. So who won the Tanenbaum–Torvalds debate? It is too soon to say (Zhou Enlai said that of the French revolution - almost 200 years after the fact) https://en.wikipedia.org/wiki/Tanenbaum%E2%80%93Torvalds_deb... The article says that the focus is on 'PCs, tablets, and high-end phones'. Wouldn't a more secure OS be relevant to server en…

It was the only thing that worked without lots of physical redundancy in high reliability. It's only thing that worked against good pentesters in high security. It's widely deployed in embedded. The monolithic OS's started copying some of its traits for their benefits but kept things in kernel mode for performance. Why? They're running on CPU's optimized for monolithic instead of microkernel designs.

So, I'd say evidence leans in favor of microkernels being better. The cutting-edge isn't that, though. It's hardware/software combinations that give more reliability and security with better usability & performance than microkernels. Lots of work in languages, compilers, and CPU extensions. CHERI and CHERIBSD is probably top example with Spin OS, JX OS or Redox OS on something like Watchdog-Lite CPU being representative of language-oriented work.

Re: Fuchsia: a new operating system

#279

Post by fauigerzigerk »

NoGravitas wrote: post #269
fauigerzigerk wrote: post #237

Earlier quoted context omitted.

In my opininon, any particular license can only be friendly or unfriendly towards particular business models but not towards business in general. Some businesses feel threatened by some open source licenses and other businesses are using the same open source licenses to do the threatening. The funding for many important open source projects comes from global corporations that use it as part of their strategy, sometim…

As to your last point, this is what the AGPL is intended to solve.

I know, but almost no one uses it.

Re: Fuchsia: a new operating system

#280

Post by nickpsecurity »

Klathmon wrote: post #44
david-given wrote: post #35

Earlier quoted context omitted.

Roughly put: in a capability based system, if you have a valid handle for a service, then you can use that service. But the only way you can get a valid handle is to ask your parent process for one --- handles are unforgeable. So your parent gets to check that you're legitimate. ...but your parent, in turn, has limited permissions, because the only way it can get a handle is to ask its parent. And when you ask your p…

That's actually really beautifully simple. Thanks for this explanation, it really helped the idea "click"

It's a simple concept whose flexibility & performing implementations can be hard. Usually takes geniuses to come up with one that works well in concept and practice. It's why Butler Lampson always thought they were a waste of time. I don't. So, here's some examples of successful application. :)

http://www.cl.cam.ac.uk/research/security/ctsrd/cheri.html

https://en.wikipedia.org/wiki/EROS_(microkernel)

Note: Definitely see KeyKOS as it was commercially deployed with both POLA and persistence of app data.

https://www.combex.com/tech/darpaBrowser.html

http://www.cs.washington.edu/homes/levy/capabook/index.html

Note: Especially see System/38 which became AS/400 & IBM i. Still selling. And they run and run and run. Architecture & POLA go a long way there.

Post reply on HN