RedoxOS

[Dmole]

Why/User Benefit/User Problem

Security!!!

Description of the feature

Kill 80% of bugs right out of the gate by using a modern language like rust

https://www.redox-os.org/news/focusing-on-rustc/

[FiretronP75]

It looks very promising! But, I don't think it is mature enough for System76 to mainstream it yet.

[Dmole]

@FiretronP75 true, but it would be nice if they helped the initiative along. Maybe $1 from each purchase or some developer time if they are already working on drivers. Maybe if they can get to the point of running Linux in a redox VM (QubesOS style).

[ilyaigpetrov]

I would like to opt out from this and save my $1 for something else.

[Dmole]

save

@ilyaigpetrov I'm sure they could write it off as tax deductable so as not too cost the customer anything.

[Kokokokoka]

Writing X in rust doesn't make X secure. It's a myth/False adv/you name it.

[Dmole]

...rust doesn't make X secure...

I claimed 80% more secure (not 100%) the claim is from historical bugs that could not have happened if modern language saifty were observed. Needlessly coding with out saifty is like clif climbing without ropes.

References; https://www.zdnet.com/article/microsoft-70-percent-of-all-security-bugs-are-memory-safety-issues/

https://ece.uwaterloo.ca/~lintan/publications/bugchar-emse14.pdf

https://source.android.com/security/bulletin

https://www.cvedetails.com/vulnerability-list/vendor_id-33/cvssscoremin-9/cvssscoremax-/Linux.html

Obligatory xkcd-s; https://xkcd.com/378/ https://xkcd.com/2030/

[Kokokokoka]

So more buzzwords without a proper claim. nice! Can you formally prove your statement (I guess not)? And also, how is rust different from f.e. safeD? What real attack vectors will rust prevent? What design choices you can do blindly while making architecture for a microkernel OS? those articles in the previous post do not form a formal proof. Also, have you read the last pdf? where is your so'called security?

[Kokokokoka]

Please, be so kind and open page 16-20 in pdf that you've provided. Your pdf contradicts with your statement. And the last one in the zdnet: % of memory-safe vs other CVE's. Do you understand the meaning of those words? Do you understand what microsoft products means? Your statement was: "Kill 80% of bugs right out of the gate by using a modern language like rust" Those articles prove nothing from your statement. They disprove at best.

[Dmole]

Can you formally prove your statement (I guess not)?

100% (N=10);

#!/bin/bash

#
# cve_scrape.sh
#

#https://nvd.nist.gov/vuln/data-feeds

curl -s https://nvd.nist.gov/feeds/json/cve/1.1/nvdcve-1.1-modified.json.gz \
    | gzip -d \
    | jq '.CVE_Items[] 
        | select(.impact.baseMetricV2.severity == "HIGH") 
        | select(.cve.description.description_data[].value 
            | contains("Linux kernel")) 
        | { severity: .impact.baseMetricV2.severity, 
            id: .cve.CVE_data_meta.ID, 
            description: .cve.description.description_data[].value } '

echo "On 2019-12-05 there were 102 Linux kernel high impact security vulnerabilities
Here is a list of the last 10 Linux CVEs and wheather Rust Could have Prevented(RCP) them;
ID,             RCP, Type
CVE-2019-9112,  yes, overflow
CVE-2019-9111,  yes, overflow
CVE-2019-9003,  yes, use-after-free
CVE-2019-8980,  yes, memory leak 
CVE-2019-8912,  yes, use-after-free
CVE-2019-3896,  yes, double-free
CVE-2019-19083, yes, Memory leaks
CVE-2019-19082, yes, Memory leaks
CVE-2019-19081, yes, memory leak
CVE-2019-19080, yes, memory leaks"

@Kokokokoka Your turn.

https://xkcd.com/386/

[Kokokokoka]

100% (N=10);

Wow, judging from a sample from 10 elements, such a nice statistics you've got here. But let's not talk about this sample and imagine for a moment that I accept this (even though you CAN'T make a statistics from a sample of 10 elems) the H_{0} was = "Kill 80% of bugs right out of the gate by using a modern language like rust". Bugs != CVE's there are many other bugs. And design bugs are bugs too. https://ece.uwaterloo.ca/~lintan/publications/bugchar-emse14.pdf This pdf had a nice preview of a good statistics. And you can clearly see that mem bugs weren't the most common ones, heck, they're one of the least common. they've got a big impact though (and I agree with that). My main point is: no language will help you designing good apps, it could prevent some (not even close to 80%) of the bugs. Neither a can language replace your injective map of codeforms. Also you somehow try to sell rust as a magic bullet: well, it's not (it reminds me of systemd evangelists and fanatics). there are other langs, like Ada, idris, safeD (ever heard of them?) (If you can prove a theorem in idris or in ada you can be sure that your code-flow is safe not only from the mem bugs, also from other design bugs. (can rust do this? (no and never will)) +rewriting something from scratch in other lang is close to exponential bug count explosion. And my answer is: qmail, libsodium, libgfxinit (https://review.coreboot.org/c/libgfxinit)

[Dmole]

@Kokokokoka The first word I wrote in this thread was "security". I clearly showed how 100% (N=10) of the most recent Linux security bugs could have been prevented with rust.

You made a point that no language (English included) can save some idiots (me, you, them) from themselves, with which I have to agree but to clarify that is not the focus of this thread. I'm not including incomplete features in my use of the term "bugs" in this security-focused thread.

[Kokokokoka]

security != CVEs, just wow. Do you understand the word DiD (take a look at openbsd: Our efforts emphasize portability, standardization, correctness, proactive security and integrated cryptography. As an example of the effect OpenBSD has, the popular OpenSSH software comes from OpenBSD. and https://www.openbsd.org/security.html)? there are other type of bugs which Rust will never prevent and Ada or idris (for example) will. Let's write a small theorem proving lang and a microkernel! also, thy most popular os is MINIX (intel me) I haven't seen any of the memory CVEs in it. There were problems, but not with MINIX, so, maybe this is more a design problem and how well one reads code and writes? this is a great project too https://bearssl.org/index.html

I clearly showed how 100% (N=10) of the most recent Linux security bugs could have been prevented with rust.

And I said that sample of 10 proves nothing as it is statistically incorrect. And you haven't read other points. If we had kernel written in idris or ada (or ocaml etc) there would have been even less problems. Time for thy functional languages to shine! By the way as far as I can remember there is a microkernel written in ocaml: https://mirage.io/ it is way better than writing it in rust or safed. http://gazagnaire.org/ens/mirage.pdf it is way safer by design. AFAIK Xen devs use it: https://xenproject.org/developers/teams/mirage-os/ https://en.wikipedia.org/wiki/Unikernel +You blindly use %. This is the most annoying part. If you would have said, that from writing in rust we would fix most of the memory bugs. there wouldn't be such a reaction from me, even worse, you don't the links that you provide or read and don't understand. You simply can't give exact numbers as it's your imagination. And you can't do a proper testing (it would involve writing several apps with the same functions by the same person and this person should forget his experience of writing other apps in test, langs which has the ability of formal proves would win)

https://www.quora.com/Could-the-Heartbleed-bug-have-happened-if-OpenSSL-had-been-written-in-Rust# https://theinvisiblethings.blogspot.com/2010/05/on-formally-verified-microkernels-and.html It seems that you don't undestand what is fp and theorem solving: https://en.wikipedia.org/wiki/ML_%28programming_language%29 https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Formal_verification in general rust is a fanboi hype-driven language this has nothing to do with a proper design and security. pps: If there is a CVE in program it doesn't mean that one is able to exploit it. So,

You made a point that no language (English included) can save some idiots (me, you, them)

Rust won't save you too. f.e. I have WASM, 3rd party js, wss, ws and some other things disabled in my browser. rust won't save from security violations of the above ones. It won't even save you from miners and from cache-layer attacks! Also, it is popular nowadays to keep passwords and open keys in mem for convenience this is bad design too.

[Dmole]

security != CVEs

CVEs are the best data available for the purposes of analysis. commit history lacks relavent deductions. Yes CVEs are almost useless for informing patch and upgrade decisions, but thats a tangent.

OpenBSD/OpenSSH

Has a great security record, but it's slow moving and small relative to Linux. I'm sure if I looked there would be a few places a safer language would have helped even this idealistic project, like this; https://nvd.nist.gov/vuln/detail/CVE-2019-16905

there are other type of bugs which Rust will never prevent and Ada or idris (for example) will.

I have never looked into either of those languages but I assume Mozilla had a reason for Rust, and there is no OS based on Ada/Idris, so also a tangent. (I'd be interested if you know of any spesifics)

MINIX

Is tiny / not comparable like l4

sample of 10

Is better O.R. than your sample of 0. Even if I did all of them for this year you would probably claim it useless due to the cve data source, but as I have countered it's the only data source and it's a good indication even in its imperfect state... If you summarize the critical CVEs for Linux this year and it differ significantly (+-10%) I'll concede my percentage estimation was wrong.

other points

I'm aware rust is not the solution to all problems however RedoxOS appears to be the most idealistic almost usable OS to invest in at the moment.

such a reaction from me

Would have been better if it contained some actual data or a preferred alternative. Because currently I am not convinced my estimation was inaccurate, or that the safety of modern languages would not benefit kernel/os security. Or that RedoxOS is not the most mature alternative.

[Kokokokoka]

In the previous post there were alternatives a) langs: safed, idris, ada, ocaml b) microkernels: minix, mirageos c) my sample is from the pdf that you've provided. It shows that you're doing misleading hypotheses d) It was your statement so it is for you to prove it (logic laws). e) using a sample of 10 and implying that this is a statistically significant is plainly wrong, from stat point of view, from argument point of view too. Anecdotal evidence != evidence. f) The fact that you're using weak statements and jump from one def of bugs to other (and i'm not even speaking of security definition yet!) neither you can state your hypothesis clearly speaks that you're impolite, and trying to troll.

Has a great security record, but it's slow moving and small relative to Linux. I'm sure if I looked there would be a few places a safer language would have helped even this idealistic project, like this;

Slow moving? care to elaborate? Still this is not an argument that i'll take. I agree, there are mem CVEs in openbsd, but still, it disproves your point of 80%. And also, one more time: Do you understand this?: "proactive defense" And this: rewriting something from scratch in other lang is close to exponential bug count explosion. +code-bloat != life. please, take a look at fsync git history in linux kernel. how it turned from a nice one to a spaghetti.

I'm aware rust is not the solution to all problems however RedoxOS appears to be the most idealistic almost usable OS to invest in at the moment.

That's a pure lie. it's only your opinion. redoxos is nothing in comparison to mirage. a) it's mature b) it's based on formal verification methods. c) it's used in production

Is tiny / not comparable like l4

this has nothing to do with correctness/etc comparison.

I have never looked into either of those languages but I assume Mozilla had a reason for Rust, and there is no OS based on Ada/Idris, so also a tangent.

Appeal to authority, sigh. So, you ignored safeD and ocaml, WOW. it's easier to read programs in D, design programs in D, make unit tests, contracts/etc -> it leads you to a better design overall as you can easily refactor your program. And there is safeD which helps you with those nasty memory bugs (this is not the entire feature list, i just wanted to name a few). you can search for projects written in ada or idris by yourself.

(I'd be interested if you know of any spesifics)

I provided links in the previous posts. It's a really good start if you'll even skim through those it would take a week (subpages too) books: D.E. Stevenson - Programming Language Fundamentals Felleisen M., Findler R.B., Flatt M., Krishnamurthi S. - How to design programs Henry S. Hacker's Delight Peter Van Roy, Seif Haridi - Concepts, techniques, and models of computer programming

Is better O.R. than your sample of 0. Even if I did all of them for this year you would probably claim it useless due to the cve data source, but as I have countered it's the only data source and it's a good indication even in its imperfect state... If you summarize the critical CVEs for Linux this year and it differ significantly (+-10%) I'll concede my percentage estimation was wrong.

You disproved yourself using this pdf already, and you ignored this point too. Do you even read what you send?

+You're blindly skipped my other arguments. So, from this point, I assume that you're trolling.

[Dmole]

MirageOS does not appear to be usable as the primary OS on a development laptop (the point of this repo/thread)

...Code can be developed on a normal OS such as Linux or MacOS X, and then compiled into a fully-standalone, specialized unikernel that runs under a Xen or KVM hypervisor...

I just reviewed 100% of the "HIGH" CVEs for this year on the Linux kernel (that system76 will be shipping) and found 100% of them could have been avoided by rust. I'll just ignore any more off topic comments in this thread because in 6 posts you have not offered a realistic alternative (BSD is a middle ground).