We need some alternative to (iOS, Android ) on mobile, something which would be secure by default, with MIT licensing model, and with Sailfish OS like swipe multitasking UI.
okay. help with the arm kernel.
4 Likes
Almost if not all phones are insecure not because of the os that runs on the application processor but the inherent vulnerability of the baseband processor… you can’t secure something when it has a gaping hole at the base.
The same is true for most recent PC platforms that have separate processor with full system acess even when the main CPU iant booted.
There’s quite a few out there but mostly commercial. The common strategy is a separation kernel that abstracts the hardware resources, lets user-mode programs communicate with IPC, wipes things like registers on context switches, hosts GUI stuff in legacy VM’s (eg Linux/Android), and runs security-critical apps directly. Redox is doing enough things right architecturally that it could be suitable for this with some modifications. The best to draw on for that is Nizza Architecture below whose most prominent implementations are OKL4 (in a “billion phones”) and GenodeOS. FOSS stuff is far from turn-key, though, as you’ll be custom integrating a pile of components of varying quality.
The other thing going on is language-based security. These usually combine a security/separation/micro-kernel with a safe language for privileged components. Started with Army Secure Operating System (ASOS) that put an A1-class kernel with an Ada runtime to let whole OS & apps be done in isolated Ada. Then JX OS did it for secure, networked OS with everything (even drivers) in a Java VM. Redox is in this category. Far as mobile, one of most advanced works would be ExpressOS below:
http://web.engr.illinois.edu/~madhu/asplos13.pdf
I can’t vouch for quality of implementation as I didn’t inspect it. Already claims to run Android browsers, etc. The important thing is the architecture combines L4 components like Genode builds on with a verifiable tooling Microsoft used in VerveOS. Anyone wanting to leverage Redox for mobile could replace the L4-related portions with Redox components, recode ExpressOS components already validated in Dafny into Rust, clean-slate a solution using concepts from both, or some other mix. Throw in Minix-3-style monitoring and restarts of drivers for extra reliability.
Point being: theres starting points for you if you want to roll up your sleeves. There’s no easy route that’s FOSS, though.
3 Likes
What do you think about exokernel principle or about Google Fuchsia/Magenta project?
1 Like
re exokernels
I honestly didn’t study exokernels much. They were competing with the approach common in high-assurance security of the time. For desktops or servers, that was a highly-assured microkernel/hypervisor + trusted components directly on it + untrusted VM’s for legacy apps with secure IPC. These worked well from pentesting to industrial practice for decades after exokernel concept was published. You could say I got my head so deep into that path that exokernels were way in my peripheral. Maybe I wrongly saw no value in them or x86 hardware was so risky we’d rather evaluate the interface to it just once. 
In today’s context, we have both server vendors and cloud companies relying increasingly on hardware features for speed or flexibility. Much like mainframes and Amiga’s of old times. They especially want this for multi-party workloads running in VM’s or containers. Exokernels allowed apps to deal with hardware directly with interfaces that made most sense to them. There’s obviously a conceptual match-up there. More designs in high-security started exploring that over past 5-7 years. I especially see value in combining an exokernel-like approach with high-assurance hardware where information flows are secured at CPU or SoC level. Already designs that do the latter formally proven down to the gates. If underlying hardware is enforcement mechanism, then the exokernel merely has to manage the system with allocations of resources, security labels for them, and error handling when hardware traps on error. Even something such as Redox could handle that with minimal code to verify. I’ve been forwarding such hardware schemes to young people looking for PhD work to hopefully increase number of new ones in future. So, definitely consider looking into combinations of secure or just small exokernels with info-flow, secure hardware for VM or container deployments.
re Google’s project
I can’t say much since there’s not too much published outside the code and some docs. I think they’re capable of making a good one but I’m always skeptical given they have no history of high-assurance security. I had to call them out when some Googlers started BS’ing about their security track record. I illustrated how little Google was doing on high-security by comparing to Microsoft Research that’s strong in high-integrity & high-security:
https://news.ycombinator.com/item?id=13567840
So, that’s my baseline seeing that they’re mostly an echo chamber of sorts that older, working methods just don’t seem to penetrate. They really need to bring in some external talent in high-assurance software, esp fielded in industry, that doesn’t think like them. Their brains mixed with that external thinking could make magic happen. If not, I predicted there was still a chance a modern project using those methods can inspire them to do something effective. They stumble on a bunch and learn by example. Appears to be happening in Magenta. I’ll note a few things I saw in the Github. Not in order of importance or anything.
-
In Relationship to LK, they indicate they know about FreeRTOS and ThreadX. These are also-ran products if you’re balancing security, performance, and flexibility. ThreadX is good in its niche, though. Claim it has user-mode distinction, object handles, and capability-security. This is similar to L4-based stuff they should be copying. OC.L4, OKL4, and seL4 are top on that space.
-
Kernel objects. They’re ref counted. In highly-assured kernels, that’s often not necessary since you know when you can safely deallocate. There’s also designs such as INTEGRITY-178B with these features: (a) separate kernel and user-mode stack (memory in general…) to isolate internal functions; (b) cool concept of any kernel call by an app requiring app to donate its own CPU and memory to accomplish it while still being metered. (b) sheilds the kernel from many memory or DOS issues caused by rogue apps. If they lack such methods or time for them, then it’s wise they’re doing reference checks as a backup. Better to address a weakness than ignore it.
-
Process and thread objects. Regular, microkernel stuff looks like. I’m neutral on this. There’s improvements in various microkernels on scheduling, IPC, thread safety, and so on. I just don’t know enough about the design to know what they’re doing, could do, and so on.
-
Handles. There’s indirection between what handles mean in reality & user-mode. That can be helpful for maintainability & security. Multiple handles available with different rights is basic, capability security. Lets you do things like avoiding giving a “root” privilege to all kinds of apps. Good they have that. Handle management is straight-forward. Rights section indicate it’s read-write-execute with added duplicate and transfer. A decent set of minimum privileges. The combo, esp with transfer, can also be used to create what are called “assured pipelines” of components that each act on a resource with minimum privilege. They are designed in a functional way for easy analysis operating on specific handle of memory. Each passes handle on once finished with validation done on data received by untrusted process.
-
Sys calls are often straight-forward but there’s a bunch of them. This means the OS will definitely have problems. They should be modelling all this in something such as ASM’s or TLA+ to catch any problems from interactions. Plus a covert channel analysis. The good side of this is they’re looking for stuff app developers would have to build themselves. Anything common and reusable can be done at the OS level where it gets more reliable over time with more verification. One less problem for app developers. Verification tech is actually good enough right now that something that size can be done right in sense of partial verification of specs, code safety, etc. They’re using C++, though, so I know they’re not doing that. There’s just not many tools to handle it with no high-assurance kernels done in C++ due to semantic complexity. Kernels such as Redox (Rust) or Muen (SPARK) doing same sys calls as Magenta will come out more secure up-front and over-time due to this.
So, that’s a brief review. They’re at least learning from capability-based microkernels along lines of L4. Missing a lot of low-hanging fruit from more robust microkernels. I think quality or security will be average for microkernel-based OS’s in that form. Way behind medium- and high-assurance microkernels using language-oriented security, model-checking, or both. Gotta get back to work. Later.
1 Like