points by westurner 1 year ago

OTOH feature ideas: Formal Verification, Process Isolation, secure coding in Rust,

- Quark is written in Coq and is formally verified. What can be learned from the design of Quark and other larger formally-verified apps.

From "Why Don't People Use Formal Methods?" (2019) https://news.ycombinator.com/item?id=18965964 :

> - "Quark : A Web Browser with a Formally Verified Kernel" (2012) (Coq, Haskell) http://goto.ucsd.edu/quark/

From https://news.ycombinator.com/item?id=37451147 :

> - "How to Discover and Prevent Linux Kernel Zero-day Exploit using Formal Verification" (2021) [w/ Coq] http://digamma.ai/blog/discover-prevent-linux-kernel-zero-da... https://news.ycombinator.com/item?id=31617335

- Rootless containers require /etc/subuids to remap uids. Browsers could run subprocesses like rootless containers in addition to namespaces and application-level sandboxing.

- Chrome and Firefox use the same pwn2own'd sandbox.

- Container-selinux and rootless containers and browser tab processes

- "Memory Sealing "Mseal" System Call Merged for Linux 6.10" (2024) https://news.ycombinator.com/item?id=40474551

- Endokernel process isolation: From "The Docker+WASM Technical Preview" https://news.ycombinator.com/item?id=33324934

- QubesOS isolates processes with VMs.

- Gvisor and Kata containers further isolate container processes

- W3C Web Worker API and W3C Service Worker API and process isolation, and resource utilization

- From "WebGPU is now available on Android" https://news.ycombinator.com/item?id=39046787 :

>> What are some ideas for UI Visual Affordances to solve for bad UX due to slow browser tabs and extensions?

>> - [ ] UBY: Browsers: Strobe the tab or extension button when it's beyond (configurable) resource usage thresholds

>> - [ ] UBY: Browsers: Vary the {color, size, fill} of the tabs according to their relative resource utilization

>> - [ ] ENH,SEC: Browsers: specify per-tab/per-domain resource quotas: CPU

- What can be learned from few methods and patterns from rust rewrites, again of larger applications

"MotorOS: a Rust-first operating system for x64 VMs" https://news.ycombinator.com/item?id=38907876 :

> "Maestro: A Linux-compatible kernel in Rust" (2023) https://news.ycombinator.com/item?id=38852360#38857185 ; redox-os, cosmic-de , Motūrus OS; MotorOS

From "Industry forms consortium to drive adoption of Rust in safety-critical systems" (2024) https://news.ycombinator.com/item?id=34743393 :

> - "The Rust Implementation of GNU Coreutils Is Becoming Remarkably Robust" https://news.ycombinator.com/item?id=34743393

> [Rust Secure Coding Guidelines, awesome-safety-critical,]