The Patreon funding starts at $4 a month. Low barrier to entry for people interested in contributing to the project. I might do it as it’s an impressive work with long-term potential. I’ve been eyeballing it as a test-case for my hypothetical Rust/SPARK method of quick verification. Also, motivation for a CompSci person (or ticki) to embed its Rust subset into Simpl to get seL4-style verification of machine code.
Is redox more stable than an OS written in C at a similar point? is it more secure? if we don’t know yet, what would it take to find out what benefits rust is adding?
Trying to use it for a few weeks on a variety of tasks. Porting some apps to it that are mostly self-contained like lightweight, server programs. However, it should already have the benefits that come with Rust such as fewer temporal, concurrency, and integration errors. I have no idea what Rust does to stop the other common 0-days like SPARK prevents in link below.
It would be helpful if one of the Rust experts on this forum to do a point-by-point comparison showing what Rust does on each weakness that SPARK is immune to. Show us what it can do & what needs work in tooling (esp static analysis). For each, whether it doesn’t stop the problem (eg covert channels), does stop the problem optionally (eg integer overflow), or does it by default (eg Borrow Checker).
The Patreon funding starts at $4 a month. Low barrier to entry for people interested in contributing to the project. I might do it as it’s an impressive work with long-term potential. I’ve been eyeballing it as a test-case for my hypothetical Rust/SPARK method of quick verification. Also, motivation for a CompSci person (or ticki) to embed its Rust subset into Simpl to get seL4-style verification of machine code.
Is redox more stable than an OS written in C at a similar point? is it more secure? if we don’t know yet, what would it take to find out what benefits rust is adding?
Trying to use it for a few weeks on a variety of tasks. Porting some apps to it that are mostly self-contained like lightweight, server programs. However, it should already have the benefits that come with Rust such as fewer temporal, concurrency, and integration errors. I have no idea what Rust does to stop the other common 0-days like SPARK prevents in link below.
https://samate.nist.gov/docs/CWEs%20Stopped%20by%20SPARK%20HCSS%20May%202011.pdf
It would be helpful if one of the Rust experts on this forum to do a point-by-point comparison showing what Rust does on each weakness that SPARK is immune to. Show us what it can do & what needs work in tooling (esp static analysis). For each, whether it doesn’t stop the problem (eg covert channels), does stop the problem optionally (eg integer overflow), or does it by default (eg Borrow Checker).
The link shows a screenshot with a Lua script filename (test.lua and colors.lua) in it. Does Redox run Lua?
Yes, and other softwares in ports repository. Ports are marked for stability in .sh files, and Lua is marked STABLE. (Many others are not.)