11 ms·

Every one of these companies except has a competing OS. Just saying.

by transitory_pce 5y ago

rvz 5y ago
'except' Who? ARM? Well [0] [0] https://github.com/ARMmbed/mbed-os https://github.com/ARMmbed/mbed-os
- pjmlp 5y ago
  Also to note, ARM toyed with the idea of using a Linux distribution as alternative to MBed, but it was short love, it is already dead, it only lasted one release. https://os.mbed.com/docs/mbed-linux-os/deprecated-product/welcome/index.html https://os.mbed.com/docs/mbed-linux-os/deprecated-product/we...
  - rvz 5y ago
    Very true. Fuchsia was also initially prototyped with a Linux kernel and well, the rest was 'history'.
    - pjmlp 5y ago
      Note that MBed Linux was created after MBed already existed, they just toyed with the idea of offering MBed userspace on top of Linux.
_wldu 5y ago
All of them are interested in good technical security (actually being secure).
- grumblenum 5y ago
  So why not formal verification or static analysis tools of an existing codebase (Frama-C)? Or dropping in C derived from a formally verified source (Idris / F-Star)? Or a language with good performance and a verified subset (Ada/Spark)? I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.
  - kaba0 5y ago
    Formal verification techniques don’t scale, not even to your average CRUD app, let alone to an OS-scale.
    - hulitu 5y ago
      Testing is hard. And (very) expensive.
      - kaba0 5y ago
        Formal verification is even harder. And even more (very) expensive.
    - tonyarkles 5y ago
      In a number of ways I'd argue that FV of an average CRUD app is a very hard problem, for two reasons: - the requirements generally change quite frequently - the requirements are generally a long way from being "formally verifiable" Where I, personally, have found the most value so far using FV techniques is from modelling "tricky" things whose requirements are quite solid. A few examples from my work: - A state machine for managing LoRa communication. The requirements in the LoRa spec are pretty good. I took those requirements and designed a state machine I could implement on a low-power device and modelled that SM in TLA+ to verify that there were no deadlocks/attempted transitions to invalid states. - A state machine for managing the Bluetooth communication between an Android app, a Bluetooth-Iridium (satellite) bridge, and the server on the other side of the Iridium link. Similar to the LoRa case, I used TLA+ to ensure that there were no deadlocks in my proposed SM (and uhh made a number of corrections as I went). Ultimately, due to the design of the BT/Iridium gateway, the exercise resulted in the conclusion that it wasn't actually possible for this process to be 100% reliable but it was possible to detect and retry the edge cases. - Modelling a somewhat awkward email/SMS invite flow for a mobile app. You could get an invitation over email or SMS, and your account transitioned through a few different states as both your email address and your phone number were verified. Modelling this helped ensure that your account couldn't get into a state where no forward progress was possible or into a state where you could use a half-completed account.
- hulitu 5y ago
  ROTFL. Microsoft is interested in security ? Maybe they shall start with their own OS. (Solar Winds, Wannacry, ransomware)
wongarsu 5y ago
Having Linux make the first move, then learn from their successes and mistakes to implement a better version in your own OS seems like a good move that profits everyone. It's not like Microsoft isn't pushing Rust on their own platform. Every time a Windows driver does a use-after-free somebody swears at Microsoft for causing a bluescreen.
- cogman10 5y ago
  From what I've heard (3rd hand :D), Rust has already made it's way into the windows kernel.
yawaramin 5y ago
Linux isn't an OS and every one of them relies on it for mission-critical infrastructure.

Every one of these companies except has a competing OS. Just saying.

rvz 5y ago

'except' Who? ARM? Well [0] [0] https://github.com/ARMmbed/mbed-os https://github.com/ARMmbed/mbed-os

pjmlp 5y ago
Also to note, ARM toyed with the idea of using a Linux distribution as alternative to MBed, but it was short love, it is already dead, it only lasted one release. https://os.mbed.com/docs/mbed-linux-os/deprecated-product/welcome/index.html https://os.mbed.com/docs/mbed-linux-os/deprecated-product/we...
- rvz 5y ago
  Very true. Fuchsia was also initially prototyped with a Linux kernel and well, the rest was 'history'.
  - pjmlp 5y ago
    Note that MBed Linux was created after MBed already existed, they just toyed with the idea of offering MBed userspace on top of Linux.

_wldu 5y ago

All of them are interested in good technical security (actually being secure).

grumblenum 5y ago
So why not formal verification or static analysis tools of an existing codebase (Frama-C)? Or dropping in C derived from a formally verified source (Idris / F-Star)? Or a language with good performance and a verified subset (Ada/Spark)? I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.
- kaba0 5y ago
  Formal verification techniques don’t scale, not even to your average CRUD app, let alone to an OS-scale.
  - hulitu 5y ago
    Testing is hard. And (very) expensive.
    - kaba0 5y ago
      Formal verification is even harder. And even more (very) expensive.
  - tonyarkles 5y ago
    In a number of ways I'd argue that FV of an average CRUD app is a very hard problem, for two reasons: - the requirements generally change quite frequently - the requirements are generally a long way from being "formally verifiable" Where I, personally, have found the most value so far using FV techniques is from modelling "tricky" things whose requirements are quite solid. A few examples from my work: - A state machine for managing LoRa communication. The requirements in the LoRa spec are pretty good. I took those requirements and designed a state machine I could implement on a low-power device and modelled that SM in TLA+ to verify that there were no deadlocks/attempted transitions to invalid states. - A state machine for managing the Bluetooth communication between an Android app, a Bluetooth-Iridium (satellite) bridge, and the server on the other side of the Iridium link. Similar to the LoRa case, I used TLA+ to ensure that there were no deadlocks in my proposed SM (and uhh made a number of corrections as I went). Ultimately, due to the design of the BT/Iridium gateway, the exercise resulted in the conclusion that it wasn't actually possible for this process to be 100% reliable but it was possible to detect and retry the edge cases. - Modelling a somewhat awkward email/SMS invite flow for a mobile app. You could get an invitation over email or SMS, and your account transitioned through a few different states as both your email address and your phone number were verified. Modelling this helped ensure that your account couldn't get into a state where no forward progress was possible or into a state where you could use a half-completed account.
hulitu 5y ago
ROTFL. Microsoft is interested in security ? Maybe they shall start with their own OS. (Solar Winds, Wannacry, ransomware)

wongarsu 5y ago

Having Linux make the first move, then learn from their successes and mistakes to implement a better version in your own OS seems like a good move that profits everyone. It's not like Microsoft isn't pushing Rust on their own platform. Every time a Windows driver does a use-after-free somebody swears at Microsoft for causing a bluescreen.

cogman10 5y ago
From what I've heard (3rd hand :D), Rust has already made it's way into the windows kernel.

yawaramin 5y ago

Linux isn't an OS and every one of them relies on it for mission-critical infrastructure.