5 ms·

Tock OS[1][2] is way more promising since it's written in Rust instead. In 2020 there is no reason to invest time in anything new in C, apart from maintaining l

by xvilka 7y ago

Tock OS[1][2] is way more promising since it's written in Rust instead. In 2020 there is no reason to invest time in anything new in C, apart from maintaining legacy software. [1] https://www.tockos.org/ https://www.tockos.org/ [2] https://github.com/tock/tock https://github.com/tock/tock

snvzz 7y ago
I'd rather seL4, which isn't written in rust but on a time-proven language (C) and yet has thorough proofs of doing what it's supposed to do, unlike this OS you suggest.
- pjmlp 7y ago
  Indeed, 40 years of proven memory corruption bugs. https://www.cvedetails.com/vulnerability-list/opmemc-1/memory-corruption.html https://www.cvedetails.com/vulnerability-list/opmemc-1/memor... https://msrc-blog.microsoft.com/2019/07/16/a-proactive-approach-to-more-secure-code/ https://msrc-blog.microsoft.com/2019/07/16/a-proactive-appro... Which are reaching the tipping point of enough is enough. Which is why Android 11 will now require memory tagging hardware for C and C++ code, when running on ARM. https://security.googleblog.com/2019/08/adopting-arm-memory-tagging-extension.html https://security.googleblog.com/2019/08/adopting-arm-memory-... https://source.android.com/devices/tech/debug/tagged-pointers https://source.android.com/devices/tech/debug/tagged-pointer... And no, it doesn't need to be Rust, in fact NVidia has decided to dump C and C++ for security critical firmware, betting on Ada, https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-autonomous-driving/ https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-auto... While F-Secure is using bare metal Go for their Foundry, https://www.f-secure.com/en/consulting/foundry https://www.f-secure.com/en/consulting/foundry Speaking of seL4, Genode OS is now using Ada alongside seL4, https://genode.org/documentation/release-notes/16.08 https://genode.org/documentation/release-notes/16.08 https://genode.org/documentation/release-notes/19.11 https://genode.org/documentation/release-notes/19.11
  - renox 7y ago
    seL4 isn't really written in C, AFAIK it's written in Haskell then translated in C. Because C is one of the few language to have a formally verified compiler CompCert. Now does seL4 support properly modern CPUs: multiple cores, with different power settings? This I don't know. And what about Spectre?
    - pjmlp 7y ago
      With the caveat that CompCert is mostly C99 and requires MISRA like C. What about Spectre? It is an hardware exploit, thus there is only so much one can don in software to prevent it. However that shouldn't be an argument for not improving the security of the IT stack, people still die when wearing security belts and helmets, but they surely do surving in higher rates than when they weren't a requirement. Exploits due to logical programming errors, false premises, hardware bugs, will always be around, however reducing the attack surface is already a big improvement.
      - renox 7y ago
        >What about Spectre? It is an hardware exploit, thus there is only so much one can don in software to prevent it. And there has been mitigations done in software in the Linux kernel (and the web browsers but that's userspace), so my question: has seL4 being updated with mitigations for Spectre? Plus for a microkernel, this can be a big performance issue..
        pjmlp 7y ago
        Mitigations never solve 100% the problems, as proven by 40 years of C related security mitigations, including hardware memory tagging. As for seL4, I only have superficial knowledge of the project.
- fork-bomber 7y ago
  I'm a seL4 fan. However I feel the need to play devil's advocate! :) seL4 may give you a formally verified kernel. However, formal verification is a dark art with very few high priests that actually understand it on the planet. Unless it becomes commoditised, it's not going to be popular. There has been some work towards that but it's still high-priest land. Unless a significant portion of the software that runs on top of that microkernel is also formally verified, there's always risk of many sorts. Oh and don't forget the fact that the hardware itself is likely not formally verified so open to attack. That's a very absolutist way of thinking and therefore not very practical I confess - but hey I was playing devil's advocate. If the Sealed Rust initiative succeeds then we may have a general purpose formal provability story at the Rust-LLVM-IR boundary thanks to the RustBelt project. That, in theory, will open the door to provably correct kernels and full stacks which I think is the right way to attack the problem.
seabird 7y ago
I'm not trying to be inflammatory, but do you realize how inadequate Rust tooling is for most embedded platforms? I'm all for embracing new technologies, but choosing to write a non-trivial embedded system using Rust on anything other than the most vanilla of ARM platforms would basically be an active attempt to sink the project.
- fork-bomber 7y ago
  The situation is no longer as dire as you imply. Cortex-M class processors have pretty robust tooling. Google chose TockOS - an RTOS written in Rust - as the foundation for their RISC-V based OpenTitan secure enclave after careful assessment of such concerns. The situation for Cortex-A isn't great but that's already trending well.
  - seabird 7y ago
    Google has immeasurable money and talent; you can choose whatever you want in that arena when you're a software company that employs nearly 100,000 people. Needless to say, most companies aren't like this. Note that I said "the most vanilla of ARM platforms." If you're using a Cortex R microcontroller like a TMS570 or RM4, using Rust means that you're now missing out on the functional-safety-standards-compliant diagnostics library and various other tooling provided by TI that is a key part of the product, but hey, at least you have a compiler. If you're using 8051, a lower-end PIC, RX, RL78, RH850, 68k, etc, you don't have a compiler at all. That's a pretty dire situation. None of this is to say that the situation can't be different in 10-20 years, but Rust is nowhere near as universally useful as C is in the embedded landscape, and that counts for a lot.
    - deleted 7y ago
      [deleted]
    - fork-bomber 7y ago
      "Google has immeasurable money..." True. In the context of this thread, note however that the risk of continued fragmentation when it comes to security enclave architecture has made Google open source a very good design in OpenTitan to woo not just deep-pocketed open source friendly chip vendors etc but also any scale of open source software shops to promote the tech. Google wouldn't go down this path unless it had very good ideas about the adoption of Rust in this space - irrespective of the scale of the entities involved and definitely considering the long-term viability of the language. "If you're using a Cortex R microcontroller..." I take your general point. However I think you may be cherry picking the functional safety argument. I agree that Rust has not penetrated functional safety ISO61508/ISO26262 domains and as such it will take a fair amount of work to get it at par with C. BTW there's efforts underway to solve that with Ferrous Systems' Sealed Rust initiative. However - and this is a contentious one - most embedded software is not written to comply to safety standards compliant. A lot of the software that is bracketed under the 'embedded' umbrella is the sort of software where the use of C today is a problem from a security standpoint and that is where Rust's value is increasingly being appreciated. Does that more general embedded software require tooling that C has but Rust doesn't ? I'd say it's quite the opposite actually. Some of the packaging, distribution and updating ease that Rust has by virtue of it's top-class tooling is something that C shall likely never have - at the language level. More specifically about Cortex-R: The Rust embedded working group has teams dedicated to Cortex-M (the most popular 'IoT' target) and the ecosystem there for bare-metal development or RTOS centric development is actually pretty rich. Try it. For Cortex-A less so but that's getting sorted slowly. There is a proposal to have a Cortex-R group now and I am confident that Cortex-R support will trend well. Again - the kind of generic tooling associated with embedded software - such as compilers, debuggers (both general and run-time specific - say for a given RTOS etc) - all of that exists already and the support for those will most certainly increase in the short term. "If you're using 8051, a lower-end PIC, RX, RL78, RH850, 68k, etc, you don't have a compiler at all. That's a pretty dire situation..." I don't disagree. I must confess I'm quite biased but I think the long term trend shall be towards a smaller set of more capable ISAs and from that standpoint I think things will converge towards the set of Arm, x86 and RISC-V, support for all of which exists in varying forms already - most very good. Totally agree that if you want to use a PIC etc then you the situation from a fundamental language support PoV is arguably dire. Personally I would future proof my design and move away from those processor choices on the double if I want to be connected - and even if not. Overall the memory safety that C has thrust upon an increasingly unsafe and insecure planet is a serious problem and I haven't seen any real scalable counters to Rust from an open, expressive, feature-rich and performant PoV.

by xvilka 7y ago

snvzz 7y ago

I'd rather seL4, which isn't written in rust but on a time-proven language (C) and yet has thorough proofs of doing what it's supposed to do, unlike this OS you suggest.

pjmlp 7y ago
Indeed, 40 years of proven memory corruption bugs. https://www.cvedetails.com/vulnerability-list/opmemc-1/memory-corruption.html https://www.cvedetails.com/vulnerability-list/opmemc-1/memor... https://msrc-blog.microsoft.com/2019/07/16/a-proactive-approach-to-more-secure-code/ https://msrc-blog.microsoft.com/2019/07/16/a-proactive-appro... Which are reaching the tipping point of enough is enough. Which is why Android 11 will now require memory tagging hardware for C and C++ code, when running on ARM. https://security.googleblog.com/2019/08/adopting-arm-memory-tagging-extension.html https://security.googleblog.com/2019/08/adopting-arm-memory-... https://source.android.com/devices/tech/debug/tagged-pointers https://source.android.com/devices/tech/debug/tagged-pointer... And no, it doesn't need to be Rust, in fact NVidia has decided to dump C and C++ for security critical firmware, betting on Ada, https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-autonomous-driving/ https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-auto... While F-Secure is using bare metal Go for their Foundry, https://www.f-secure.com/en/consulting/foundry https://www.f-secure.com/en/consulting/foundry Speaking of seL4, Genode OS is now using Ada alongside seL4, https://genode.org/documentation/release-notes/16.08 https://genode.org/documentation/release-notes/16.08 https://genode.org/documentation/release-notes/19.11 https://genode.org/documentation/release-notes/19.11
- renox 7y ago
  seL4 isn't really written in C, AFAIK it's written in Haskell then translated in C. Because C is one of the few language to have a formally verified compiler CompCert. Now does seL4 support properly modern CPUs: multiple cores, with different power settings? This I don't know. And what about Spectre?
  - pjmlp 7y ago
    With the caveat that CompCert is mostly C99 and requires MISRA like C. What about Spectre? It is an hardware exploit, thus there is only so much one can don in software to prevent it. However that shouldn't be an argument for not improving the security of the IT stack, people still die when wearing security belts and helmets, but they surely do surving in higher rates than when they weren't a requirement. Exploits due to logical programming errors, false premises, hardware bugs, will always be around, however reducing the attack surface is already a big improvement.
    - renox 7y ago
      >What about Spectre? It is an hardware exploit, thus there is only so much one can don in software to prevent it. And there has been mitigations done in software in the Linux kernel (and the web browsers but that's userspace), so my question: has seL4 being updated with mitigations for Spectre? Plus for a microkernel, this can be a big performance issue..
      - pjmlp 7y ago
        Mitigations never solve 100% the problems, as proven by 40 years of C related security mitigations, including hardware memory tagging. As for seL4, I only have superficial knowledge of the project.
fork-bomber 7y ago
I'm a seL4 fan. However I feel the need to play devil's advocate! :) seL4 may give you a formally verified kernel. However, formal verification is a dark art with very few high priests that actually understand it on the planet. Unless it becomes commoditised, it's not going to be popular. There has been some work towards that but it's still high-priest land. Unless a significant portion of the software that runs on top of that microkernel is also formally verified, there's always risk of many sorts. Oh and don't forget the fact that the hardware itself is likely not formally verified so open to attack. That's a very absolutist way of thinking and therefore not very practical I confess - but hey I was playing devil's advocate. If the Sealed Rust initiative succeeds then we may have a general purpose formal provability story at the Rust-LLVM-IR boundary thanks to the RustBelt project. That, in theory, will open the door to provably correct kernels and full stacks which I think is the right way to attack the problem.

seabird 7y ago

I'm not trying to be inflammatory, but do you realize how inadequate Rust tooling is for most embedded platforms? I'm all for embracing new technologies, but choosing to write a non-trivial embedded system using Rust on anything other than the most vanilla of ARM platforms would basically be an active attempt to sink the project.

fork-bomber 7y ago
The situation is no longer as dire as you imply. Cortex-M class processors have pretty robust tooling. Google chose TockOS - an RTOS written in Rust - as the foundation for their RISC-V based OpenTitan secure enclave after careful assessment of such concerns. The situation for Cortex-A isn't great but that's already trending well.
- seabird 7y ago
  Google has immeasurable money and talent; you can choose whatever you want in that arena when you're a software company that employs nearly 100,000 people. Needless to say, most companies aren't like this. Note that I said "the most vanilla of ARM platforms." If you're using a Cortex R microcontroller like a TMS570 or RM4, using Rust means that you're now missing out on the functional-safety-standards-compliant diagnostics library and various other tooling provided by TI that is a key part of the product, but hey, at least you have a compiler. If you're using 8051, a lower-end PIC, RX, RL78, RH850, 68k, etc, you don't have a compiler at all. That's a pretty dire situation. None of this is to say that the situation can't be different in 10-20 years, but Rust is nowhere near as universally useful as C is in the embedded landscape, and that counts for a lot.
  - deleted 7y ago
    [deleted]
  - fork-bomber 7y ago
    "Google has immeasurable money..." True. In the context of this thread, note however that the risk of continued fragmentation when it comes to security enclave architecture has made Google open source a very good design in OpenTitan to woo not just deep-pocketed open source friendly chip vendors etc but also any scale of open source software shops to promote the tech. Google wouldn't go down this path unless it had very good ideas about the adoption of Rust in this space - irrespective of the scale of the entities involved and definitely considering the long-term viability of the language. "If you're using a Cortex R microcontroller..." I take your general point. However I think you may be cherry picking the functional safety argument. I agree that Rust has not penetrated functional safety ISO61508/ISO26262 domains and as such it will take a fair amount of work to get it at par with C. BTW there's efforts underway to solve that with Ferrous Systems' Sealed Rust initiative. However - and this is a contentious one - most embedded software is not written to comply to safety standards compliant. A lot of the software that is bracketed under the 'embedded' umbrella is the sort of software where the use of C today is a problem from a security standpoint and that is where Rust's value is increasingly being appreciated. Does that more general embedded software require tooling that C has but Rust doesn't ? I'd say it's quite the opposite actually. Some of the packaging, distribution and updating ease that Rust has by virtue of it's top-class tooling is something that C shall likely never have - at the language level. More specifically about Cortex-R: The Rust embedded working group has teams dedicated to Cortex-M (the most popular 'IoT' target) and the ecosystem there for bare-metal development or RTOS centric development is actually pretty rich. Try it. For Cortex-A less so but that's getting sorted slowly. There is a proposal to have a Cortex-R group now and I am confident that Cortex-R support will trend well. Again - the kind of generic tooling associated with embedded software - such as compilers, debuggers (both general and run-time specific - say for a given RTOS etc) - all of that exists already and the support for those will most certainly increase in the short term. "If you're using 8051, a lower-end PIC, RX, RL78, RH850, 68k, etc, you don't have a compiler at all. That's a pretty dire situation..." I don't disagree. I must confess I'm quite biased but I think the long term trend shall be towards a smaller set of more capable ISAs and from that standpoint I think things will converge towards the set of Arm, x86 and RISC-V, support for all of which exists in varying forms already - most very good. Totally agree that if you want to use a PIC etc then you the situation from a fundamental language support PoV is arguably dire. Personally I would future proof my design and move away from those processor choices on the double if I want to be connected - and even if not. Overall the memory safety that C has thrust upon an increasingly unsafe and insecure planet is a serious problem and I haven't seen any real scalable counters to Rust from an open, expressive, feature-rich and performant PoV.