# Threads for karjudev

1. 2

I’d like to completely reimagine, redesign and reimplement a modern operative systems that, learned the lessons of UNIX, Linux etc. would be centered about modern concepts in computer science (no more “everything is a file”), designed for the interoperability between desktop, mobile and IoT. It’s more about creating a new, more modern and mature standard that can overcome POSIX, Windows, Mac/iOS (BSD) and the bizarre Android SDK, and then develop a whole new OS that learned from all these lessons.

1. 6

Let me argue in favour of learned indexes by spamming the PGM-index, the (AFAIK) only learned data structure with formal worst-case query time guarantees.

1. 1

Working on my BSc thesis on privacy risk assessment in text mining and planning a series of blog posts about Data Driven Fantasy Football for the next season.

1. 2

Really nice article, @karjudev, but I noticed one small issue/error: The formula for the page rank z_i is malformed in that the sum-index is not under the sigma but right next to it instead.

1. 2

Thank you for your appreciation! Actually the formula is well formed in LaTeX: z_i = \sum_{j \in \mathcal{I}_i} P_{ij} z_j. This could be a issue with KaTex on Dev.to that renders badly apexes and subscripts.

1. 24

Hackerism strikes again. Linux is not gonna save us from Google/Apple, but a serious project with focus on UI/UX, backed by little (cooperative?) manufacturers and a solid ecosystem will do. Let’s make a mobile OS for everyone, not just put Linux on the phone.

1. 14

That was my issue with so many of these Linux phones - the phone isn’t interesting just because it has Linux on it. A Nokia N900 was a great phone because it had UX polish, an ecosystem, and quality hardware and software. Otherwise, you get something uninteresting like a Freerunner.

1. 3

I never had a N900, but I did have the N9 successor, and to this day it’s probably the best phone I ever had UX-wise.

But … WhatsApp didn’t make an app for it, so eventually it was kinda useless as I couldn’t talk to my friends. Unfortunatly, building a viable non-Android/iOS phone is much harder than building just a good phone. Microsoft discovered this as well.

1. 3

I loved my N900. And I loved my Windows Phone after that. Android is still a slum compared to either of these, sadly; it did get better than it used to be a decade ago, at least. (If I can’t have a Librem 5 or it’s not feasible to use/any good (likely, sadly), it’s the new iPhone SE for me.)

1. 3

I just get the cheapest phones I can find these days; I tend to lose/break them anyway. I currently have a Galaxy A2 Core for about €70 which runs on Android Go, and it actually works surprisingly well. The only thing I miss is that the screen doesn’t light up on notifications.

2. 9

Linux is not the right choice at all to begin with, which is why Google is working on Fuchsia.

The monolithic kernel approach prevents any hope of security or responsiveness, as the kernel is huge, runs fully privileged and would be impossible in practice to formally verify to be secure and to be able to meet some hard realtime deadline, no matter how high (like, years) you set this deadline; The kernel might never yield the cpu. There’s simply no proof it ever will.

In contrast, seL4 is formally proven. It can enforce separation, and the kernel grab on the cpu will never exceed the WCET.

It is by no means easy to build a sizable secure system or realtime system. But at the very least it is possible to do so with the microkernel multiserver approach. It simply isn’t with Linux.

1. 8

The monolithic kernel approach prevents any hope of security or responsiveness, as the kernel is huge, runs fully privileged and would be impossible in practice to formally verify to be secure

I’d be interested in an analysis of reported Android security bugs cross-referenced to where they ultimately occurred: in the kernel, in a specific kernel subsystem, or module, or in a layer above the kernel. I think, but don’t know, that we’d find that very few of them were ultimately in the kernel at all.

I appreciate your comment was really about formal verification. Is the iOS kernel formally verified? Or any smartphone kernel past or present?

1. 7

Is the iOS kernel formally verified? Or any smartphone kernel past or present?

As far as I am aware, no and no.

There’s much yet to be done in the operating systems field.

2. 8

In short: Linux can be used just fine for systems like this, monolithic and unverified as it is. The proof is, after all, in the pudding, not in the recipe used to make it.

Longer: Theoretically those verified systems do have several advantages when it comes to designing secure (in all the meanings of the word) products but thus far this theoretical advantage has failed to pan out at scale in real-life systems. Why is that? Ever since the inception of Linux and the well-known spat between Tannenbaum and Torvalds this discussion has been going on while Linux spread like wildfire. In that period a whole host of theoretically-superior-when-it-comes-to-security systems has seen the light… and failed to thrive. Why is this? What makes Linux (and similarly ‘evolved, not designed’) systems thrive while these alternatives wither on the vine? Is it just the unwillingness of the market to invest in alternative solutions? If that were the case I’d have expected at least one of these alternative systems to have thrived in the alternate world of academia but this has not happened.

I suspect the reasons are many:

• evolved systems consistently outperform designed systems
• lack of hardware support (a.k.a. ‘drivers’) keeps designed systems back, partly due to the need for formal verification - a system is a strong as its weakest link
• verified systems and proprietary software do not mix - no binary blobs in verified systems…
• …leading to even less hardware support because vendors don’t want to expose their ‘intellectual property’ for all to see
• to make a difference in real life, everything needs to be designed and verified, from the ‘kernel’ (in whatever form or shape, from monolithic to micro to whatever) to that silly little clipboard app which suddenly got popular, otherwise the resulting product will still leak data to the adversary. Who gets to be the gatekeeper to separate the chaff from the grain? The user? Some benevolent overlord? In the former case many users will just install the damn app because of reasons and poof there goes trust. In the latter case a new apple or google or big brother just saw the light.
• more reasons: _________________ (fill in the blanks)

Anyway, given the open nature of this new crop of hardware - Librem, Pine, etc - the chance of proving the merits of these designed systems is there, may the next Linux Torvalds rise to make fame as the one who managed to launch seL4 or any of the other candidates into the main stream. Until such time, Linux will do just fine.

1. 6

If that were the case I’d have expected at least one of these alternative systems to have thrived in the alternate world of academia but this has not happened.

Microkernel, multiserver systems are widely deployed, just not very visible.

Much progress has been done in the operating systems field. Tunnel vision manifests as only seeing Linux’s progress, and being blind to everything else that’s been going on.

A valuable resource on the topic is Gernot Heiser’s blog, for anyone who wishes to get started.

Ever since the inception of Linux and the well-known spat between Tannenbaum and Torvalds this discussion has been going on while Linux spread like wildfire.

For anyone who hasn’t read it, here’s the last installment.

The proof is, after all, in the pudding

No, it isn’t. Dressing Linux up nicely won’t change the fact it is not suitable. Google has discovered this already (Fuchsia), so has Huawei (HarmonyOS).

evolved systems consistently outperform designed systems

Linux is fundamentally incapable of security and of hard realtime. No amount of duct tape will change the fundamental facts of a system.

to make a difference in real life, everything needs to be designed and verified

Actually, this is not the case. Once isolation can be enforced (as seL4 manages to) and assuming the system is modeled around capabilities (Not to be confused with POSIX capabilities. There’s a good introduction to capabilities in Genode’s Book), mitigation actually works. Nothing can overstep its capabilities as the system actually mandates so.

silly little clipboard app

Would have a hard time justifying it needs access to the network (to leak your data). Just requesting such capability would quickly flag the app suspicious. Monitoring what the app does is also much easier when the capabilities it gets do come from wrappers designed for the purpose. The clipboard app would only see an interface, and have a hard time determining what the implementation is.

1. 1

The silly little clipboard app will want network access to allow it to react ‘intelligently’ to whatever is on your clipboard so it can do its thing - translate the contents, find better prices for the product you just marked, suggest alternative sources for the marked content, tell them which of their friends marked similar content, etc. People will say ‘OK’ when confronted with the choice to allow or deny network access, after all they want that silly app to work.

When confronted with fool-proof systems, \${god} reacts by creating better fools.

1. 5

If we accept the assumption that user is able to at the very least avoid sabotaging themselves by giving away all the keys, we can end this “no system can protect against user stupidity” tangent I won’t follow you further down with.

Then we can go back to discussing whether Linux’s design is a good fit. My take is, as you know, that it is not.

2. 4

The monolithic kernel approach prevents any hope of security or responsiveness, as the kernel is huge, runs fully privileged

Even (NeXT/)Apple who pushed a microkernel (Mach) towards a monolithic kernel is now migrating to user-space drivers and networking extensions for security reasons.

1. 5

NeXT always ran Mach in a single-server model. In this mode, Mach is basically a hardware abstraction layer, not a microkernel. Most monolithic kernels have adopted similar layering (and, in the BSD world, pulled in a lot from Mach) but there’s no real advantage to having isolation between a HAL and a single security context running on top of it, so this largely went away.

Single-server Mach is much closer to a hypervisor than what most people think of as a microkernel and hypervisors are incredibly common. Even Android is moving towards having a hypervisor (hafnium) under Linux to run the security-critical things in a non-Linux VM.

1. 4

NeXT always ran Mach in a single-server model. In this mode, Mach is basically a hardware abstraction layer, not a microkernel.

I never meant to suggest that they ever used it differently than a single server kernel. This is well-documented history. I should have completely left out this comment. It was more meant as a nod towards Mach’s original development goal [1] to make a microkernel (and things are going more towards that direction again). Even though they only reached that goal with Mach 3.0 (which was too slow to be a practical UNIX kernel anyway).

[1] I may be wrong there, I always thought that this was one of their original goals, but maybe this was only a goal of Mach 3.0?

2. 3

Even (NeXT/)Apple who pushed a microkernel (Mach) towards a monolithic kernel

Mach is a first generation microkernel or so called pre-Liedtke. The context switch cost of Mach is horrendous, thus it is seldom used in a multiserver configuration.

NeXT did what they had to do at the time, and Apple could have switched to L4 or some other post-Liedtke kernel, but they unfortunately have not.

Linux is also slowly getting more interfaces and optimizations to “run drivers and subsystems in userspace”, but as with Mach, it is ill-suited for this.

The whole industry will move past Monolithic kernels. Give it time.

1. 3

Mach is a first generation microkernel or so called pre-Liedtke. The context switch cost of Mach is horrendous, thus it is seldom used in a multiserver configuration.

Sure. But it seems that they want to move things that they have traditionally had in kernel space to user space, but probably find it more attractive to gradually morph their kernel into something more secure than doing an abrupt rebase of their system. Which makes Fuchsia all the more impressive, but we have to see when/if Android actually switches to Fuchsia.

That said…

NeXT did what they had to do at the time, and Apple could have switched to L4 or some other post-Liedtke kernel, but they unfortunately have not.

Apple is no stranger to L4, since their secure enclave runs an L4-based OS, so every recent iDevice/Mac is running L4, just like any modern Intel CPU with ME is running Minix :p:

https://support.apple.com/guide/security/dedicated-boot-rom-and-anti-replay-services-sec0fe6a5c39/web

2. 5

Let’s make a mobile OS for everyone, not just put Linux on the phone.

But isn’t putting Linux (or some free-as-in-freedom OS) on the phone the very first step? Perhaps I misread the implication, but I think what you (and others) are saying is that projects like Librem are a net negative, whereas in my opinion they are a huge leap forward.

1. 1

Almost none of the buttons work ?

1. 1

It’s actually under construction, the only working section is the filter

1. 3

Not much, but I’m in the core team of Gambe.ro, the Italian Lobsters fork, and I’m developing a Twitter bot for Gambe.ro that is extensible with other social network/platforms and is compatible with every Lobsters fork that exposes a JSON feed.

1. 1

It looks like a wrapper for C that solves some of its problems, but, except for something, I think that It could be done with some macros.