Journal KataOS, un OS sécurisé basé sur SeL4 écrit en Rust ... par Google

Posté par  (site web personnel, Mastodon) . Licence CC By‑SA.
27
19
oct.
2022

Cher journal,

Depuis le temps que j’apprends le Rust, je me demandais pourquoi il n'y avait pas de système d'exploitation dans ce langage, surtout dans l'embarqué. En effet, la protection mémoire et les nombreuses vérifications faites à la compilation en font un super langage pour l'embarqué où il est toujours compliqué de déverminer «en live» via des sondes et autre débuggers.

Tous les FreeRTOS, Zephyr et autre Nuttx se basent tous sur le langage C que ça soit pour écrire le cœur du système ou les applications.

On a cependant vu les choses bouger avec l'intégration de Rust dans la dernière version de Linux et il semble être possible d'écrire des applications en Rust pour Zephyr.

Quand a un OS écrit directement en Rust, cela reste pour le moment à l'état de projet avec RustOS ou Redox.

Mais aujourd'hui j’apprends que Google publie un projet d'OS temps réel sécurisé et certifié écrit en Rust !

L'OS, nommé KataOS se base sur le micro-kernel SeL4 pour proposer une solution temps réel et certifié de système d'exploitation pour l'embarqué (On dit IoT pour Internet des Objets si on veut être dans le vent).

Je suis étonné de voir Google promouvoir le Rust au détriment du Go. Il faut croire que ces deux langages ne ciblent pas tout à fait les même marchés.

C'est en tout cas une affaire à suivre.

  • # Combien de temps avant son abandon ?

    Posté par  . Évalué à 10.

    J'espère me tromper mais Google commence à avoir le meme track record que Mozilla pour les projets abandonnés. Y a quelques années ça faisait beaucoup de bruit autour de FushiaOS, on en entendais même certains le prédire en remplaçant de Linux pour Android. Aujourd'hui FushiaOS reste un jouet et le restera certainement pour toujours, y a pas d'écosystème autour.

    Je pense aussi au projet Ara avec le protocole greybus, beaucoup de travail, code mainliné par Greg K.H, idée sympa etc… Le projet a été tué avant sa sortie.

    Donc bon, je vais continuer à mettre un billet sur Zephyr pour les prochaines années, ça me semble un choix bien plus sur.

    • [^] # Re: Combien de temps avant son abandon ?

      Posté par  (site web personnel, Mastodon) . Évalué à 4.

      Aujourd'hui FushiaOS reste un jouet et le restera certainement pour toujours, y a pas d'écosystème autour.

      Tu penses ? J'ai vu que c'était déployé sur les Nest Hub, je ne sais pas si on peut encore parler de "jouet".

      • [^] # Re: Combien de temps avant son abandon ?

        Posté par  . Évalué à 5.

        Merci j'avais raté l'info concernant le Google Nest Hub. Donc oui le terme "jouet" est un peu trop fort. Mon point sur le manque d'un écosystème autour reste valable. Un seul projet commercial fait par google lui même. Je miserai pas mes propres projets embarqués la dessus, Zephyr me semble un choix bien plus pertinent et pérenne.
        Après je peux me tromper et j'aimerai me tromper car techniquement ce que propose Fushia est intéressant. Y a quelques années j'avais misé sur Mbed pour la force de l'écosystème qu'il avait embarqué autour de lui. Bon c'est plus le cas aujourd'hui. Les quelques trucs intéressant comme litteFS sont aujourd'hui repris dans Zephyr.

        • [^] # Re: Combien de temps avant son abandon ?

          Posté par  (site web personnel, Mastodon) . Évalué à 2.

          Je suis d'accord que Google lance beaucoup de projet et en développe peu jusqu'au bout. Néanmoins c'est possible.
          De toutes manière avant de se lancer à utiliser réellement un projet il faut un certains background que KataOS n'a pas évidemment.

          Sous licence Creative common. Lisez, copiez, modifiez faites en ce que vous voulez.

    • [^] # Re: Combien de temps avant son abandon ?

      Posté par  (site web personnel) . Évalué à 7. Dernière modification le 19 octobre 2022 à 10:41.

      La, c'est de la R&D (ça sort de Google Research), donc ç'est aussi normal d'essayer des choses, et parfois de les abandonner.

      C'est même le propre du logiciel libre que de faire des choses de façon ouverte.

      Si ça venait à être présenté comme un produit, ça serait différent, mais je pense pas qu'on puisse blamer Mozilla ou Google pour des logiciels libres mis à disposition, ou du moins, pas autant que pour l'abandon de Stadia, Wave ou d'autres produits mis en avant en grande pompe.

    • [^] # Re: Combien de temps avant son abandon ?

      Posté par  . Évalué à 4.

      J'étais tombé sur un article expliquant que chez Google c'est courant de voir des projets aussitôt abandonnés une fois sorti. En gros, les équipes ont des primes pour chaque projet mis en prod. Du coup, le principe c'est de participer à un projet, et une fois sorti, de le quitter et de passer à un autre en cours de développement. Ceux qui restent ne sont du coup pas les personnes les plus compétentes du projet, qui finira très probablement abandonné.

      Emacs le fait depuis 30 ans.

      • [^] # Re: Combien de temps avant son abandon ?

        Posté par  (Mastodon) . Évalué à 3.

        J'étais tombé sur un article expliquant que chez Google c'est courant de voir des projets aussitôt abandonnés une fois sorti.

        Je crois qu'on tient une belle liste, là : https://killedbygoogle.com/

      • [^] # Re: Combien de temps avant son abandon ?

        Posté par  . Évalué à 7.

        Pas une prime en soit. Mais leur système interne de promotion requiert entre autre que l’employé mette en place un dossier expliquant pourquoi ils doivent être promus.

        Et dans ces dossiers, dire que t’as a été un élément clé du lancement d’un nouveau produit a beaucoup plus de poids que de dire que t’as maintenu un produit existant.

        En pratique, ça crée une incentive perverse, ou les employés motivés pour gravir les échelons vont faire en sorte de pousser pour des gros trucs qui claquent dans les dossiers de promotions, plutôt que de faire en sorte que ce qui existe continue de bien marcher et à du succès. Que ce soit pour les ingénieurs ou les product managers.

        Ceux qui restent ne sont pas forcément mauvais. Ils ont juste les dents moins longues et ont des motivations différentes qu’avancer leur carrière a vitesse grand V que ceux qui poussent pour de gros projets.

        Linuxfr, le portail francais du logiciel libre et du neo nazisme.

    • [^] # Re: Combien de temps avant son abandon ?

      Posté par  (site web personnel, Mastodon) . Évalué à 2.

      Donc bon, je vais continuer à mettre un billet sur Zephyr pour les prochaines années, ça me semble un choix bien plus sur.

      Pour le moment c'est certainement le meilleurs choix pour faire de l'embarqué communiquant. Par contre si l'on veut de la sureté et de la sécurité je ne suis pas sûr qu'on puisse facilement certifier un produit avec Zephyr.

      J'ai plus qu'une balle

  • # Face au nouveau joujou du Grand Ami, je n'ai plus qu'une chose à dire

    Posté par  . Évalué à 3.

    Ça va être la Kata !

    C'est tout pour moi. :3

  • # Nuances

    Posté par  . Évalué à 9.

    Qu'on me corrige au besoin (j'ai à peine touché à l'embarqué en jouant avec de l'arduino), mais l'OS n'est pas vraiment certifié, seul le micro kernel (Sel4) l'est, et l'était déjà avant l'arrivée de google avec Rust.

    De mon point de vue, cet OS est plutôt un framework qui inclus un lib pour communiquer avec le kernel et qui vient avec quelques fonctions supplémentaires utiles (loggers, custom allocators, ..). Mais j'imagine que c'est ce qu'on appelle un OS à ce niveau :-)

    • [^] # Re: Nuances

      Posté par  (site web personnel, Mastodon) . Évalué à 5.

      Je dirais même plus : SeL4 est écrit en C (https://github.com/seL4/seL4/tree/master/src/kernel). Alors si KataOS se base dessus, ce n'est pas un OS écrit en Rust. Je pense qu'il part de KataOS et après possède l'interface pour coder les librairies en Rust… Il y a une diférence.

      Sous licence Creative common. Lisez, copiez, modifiez faites en ce que vous voulez.

    • [^] # Re: Nuances

      Posté par  (site web personnel, Mastodon) . Évalué à 4. Dernière modification le 20 octobre 2022 à 09:35.

      Qu'on me corrige au besoin (j'ai à peine touché à l'embarqué en jouant avec de l'arduino), mais l'OS n'est pas vraiment certifié, seul le micro kernel (Sel4) l'est, et l'était déjà avant l'arrivée de google avec Rust.

      Tout à fait, et si l'on veut être tatillon je dirais même que Sel4 n'est pas certifié non plus puisque c'est l'ensemble du système que l'on certifie.

      Il vaudrait mieux parler d'OS «certifiable».

      De mon point de vue, cet OS est plutôt un framework qui inclus un lib pour communiquer avec le kernel et qui vient avec quelques fonctions supplémentaires utiles (loggers, custom allocators, ..). Mais j'imagine que c'est ce qu'on appelle un OS à ce niveau :-)

      On est proche du débat GNU/Linux. Peut-être devrait-on parler de distribution Sel4 pour le coup ?

      J'ai plus qu'une balle

  • # Go et Rust

    Posté par  (site web personnel) . Évalué à 7.

    Je suis étonné de voir Google promouvoir le Rust au détriment
    du Go. Il faut croire que ces deux langages ne ciblent pas tout
    à fait les même marchés.

    Bien que tu puisses faire du Go pour de l'embarqué et des MCU, fondamentalement, ça n'est pas le plus adapté. Par exemple, Go utilise un garbage collector (même si il vient sans VM, contrairement à Java), ce qui le rends moins prévisible au niveau de la gestion mémoire (vu que, sauf erreur de ma part, c'est fait via un thread séparé).

    Rust est un peu plus bas niveau dans le sens ou la gestion de la mémoire est fait via le language (le borrow checker, les scopes, etc), via des mécanismes plus proches du C, alors que Go semble approcher ça par l'approche plus haut niveau (eg, comme Java, python).

    Cela implique en effet différents choix de design.

    Mais bon, faut pas croire que les ingés de Google sont forcés de faire de la recherche en utilisant les logiciels écrits par d'autres ingés. C'est une vision assez tribale d'une entreprise qui ne correspond pas à la réalité.

    • [^] # Re: Go et Rust

      Posté par  (site web personnel) . Évalué à 6.

      https://tinygo.org/docs/concepts/faq/why-go-instead-of-rust/

      Le post ci-dessus est une grosse connerie, ne le lisez pas sérieusement.

    • [^] # Re: Go et Rust

      Posté par  (site web personnel) . Évalué à 4.

      "Bien que tu puisses faire du Go pour de l'embarqué et des MCU, fondamentalement, ça n'est pas le plus adapté."

      Sur un Linux "embarqué" (OpenWRT), un helloworld en GO faisait 1.6MB.

      Je n'ai pas reessayé depuis, mais c'était une catastrophe à l'époque. Le stripping ne fonctionnait pas bien non plus.

      • [^] # Re: Go et Rust

        Posté par  (site web personnel) . Évalué à 3.

        Ensuite, c'est "hello world". C'est important de voir à quel point tu peux optimiser bien sur, mais il faut aussi voir avec des cas plus réalistes, ou tu va devoir de toute façon rajouter des libs et ou l'écart va se réduire.

        Et même si je comprends l'argument de gagner autant que possible des ressources, il y a aussi des limites à ça.

        Si je cible, par exemple, un ESP32 avec 4M de flash, j'ai pas besoin de pinailler sur les Ko, ni même sur 1 Mo suivant ce que je vais faire.

        Je suis sur que si j'ai assez de ressources, je peux trouver des ESP32 avec 2M de flash et sans doute faire des économies à ce niveau. Mais peut être que j'aurais ni le volume, ni le temps pour ça. C'est cool d'avoir un programme qui fait que 512 Ko au lieu d'un qui fait 1.5 Mo, mais si au final, ça me coûte pareil en hardware parce qu'on trouve pas de plateforme sur le marché avec moins de 2 Mo, ça réduit pas mal l'attrait à priori.

        Curieusement, je trouve que ça a plus d'importance sur les serveurs et le cloud, vu que les ressources sont plus souvent partagés avec plus de granularité (eg, il y a autre chose que des cases ou on passe de X à 2X), mais à une autre échelle (dans le sens ou on se préoccupe pas des soucis à l'échelle du Mo).

      • [^] # Re: Go et Rust

        Posté par  . Évalué à 3.

        Pour réduire la taille de binaire GO pour de l'embarqué, j'utilise UPX pour info : https://github.com/upx/upx . Tu as une légère pénalité au démarrage due à la décompression mais ça remplie plutôt bien son role.

        Et concernant le fait que Rust soit plus adapté niveau mémoire pour faire du bas niveau ça dépends des cas, qu'on on veut vraiment optimiser le rendu assembleur du code pour le moment y a de grosse surprise sur les choix que fait le compilateur Rust. Voir pour plus d'info : https://lwn.net/Articles/907876/ ou https://twitter.com/LinaAsahi/status/1567752082060619776

  • # go vs rust et google

    Posté par  (Mastodon) . Évalué à 7.

    Go et Rust n'ont pas vraiment les même spécificités ni les mêmes buts, je ne vois pas pourquoi Google, qui fait aussi du developpement dans d'autres langage, devrait ignorer rust. D'autant plus que go n'est pas un projet qu'ils commercialisent en tant que tel.

  • # OS en Rust

    Posté par  . Évalué à 6.

    je me demandais pourquoi il n'y avait pas de système d'exploitation dans ce langage, surtout dans l'embarqué.

    Tu as du passer à coté de Redox c'est un OS pour le bureau entièrement en Rust qui semble quazi fonctionnel.

    Pour l'embarqué il y a drone os et tock qui on l'air de tirer leur épingle du jeu.

    Je n'ai pas encore pu les tester par manque de temps mais ça viendra.

    • [^] # Re: OS en Rust

      Posté par  . Évalué à 5.

      Redox est cité dans le journal…

      « Le pouvoir des Tripodes dépendait de la résignation des hommes à l'esclavage. » -- John Christopher

      • [^] # Re: OS en Rust

        Posté par  . Évalué à 5.

        Exact, un de ces jours il faudra que j'apprenne à lire les énoncés en entier avant de répondre.

    • [^] # Re: OS en Rust

      Posté par  (site web personnel, Mastodon) . Évalué à 4.

      Tu as du passer à coté de Redox c'est un OS pour le bureau entièrement en Rust qui semble quazi fonctionnel

      En fait, quasi en Rust. Si tu regardes le code source :

      • redoxfs est en pur Rust
      • relibc est à 63% en Rust mais dépend d'autres libs dont certaines comme pthreads-emb ou openlibm sont en C à 100% ou core_io qui est en partie en C

      Ça reste très bien mais de là à dire que c'est entièrement en Rust, y a un pas et pas un petit.
      Écrire un OS complet, ça reste une tâche énorme.

      • [^] # Re: OS en Rust

        Posté par  (site web personnel, Mastodon) . Évalué à 2.

        Tu as du passer à coté de Redox c'est un OS pour le bureau entièrement en Rust qui semble quazi fonctionnel.

        J'en ai parlé dans le journal. En même temps Redox ne joue par vraiment dans la même cour que KataOS.

        Dans un cas on a un OS «générique» pour faire tourner de multiples applications sur un gros processeur avec beaucoup de RAM.

        Et dans l'autre cas on parle vraiment d'un système embarqué sur microcontrôleur avec quelques tâches temps réel et une certaine sûreté de fonctionnement.

        J'ai plus qu'une balle

  • # SeL4

    Posté par  (site web personnel, Mastodon) . Évalué à 4.

    SeL4 est écrit en C (https://github.com/seL4/seL4/tree/master/src/kernel). Alors si KataOS se base dessus, ce n'est pas un OS écrit en Rust. Je pense qu'il part de KataOS et après possède l'interface pour coder les librairies en Rust… Il y a une diférence.

    Sous licence Creative common. Lisez, copiez, modifiez faites en ce que vous voulez.

    • [^] # Re: SeL4

      Posté par  (site web personnel, Mastodon) . Évalué à 1.

      J'ai vu qu'@Elfir3 arrive à la même conclusion avec son commentaire "Nuances"

      Sous licence Creative common. Lisez, copiez, modifiez faites en ce que vous voulez.

      • [^] # Re: SeL4

        Posté par  . Évalué à 8.

        Bah, seL4 ça n'est pas juste du C, c'est du C+des preuves formelles qui fournissent plus d'"assurances" que Rust.
        Et en plus avec le C, il existe un compilateur "prouvé formellement" CompCert, chose que Rust n'a pas donc tout bug du compilateur Rust peut impacter ta sécurité..

        Sauf qu'évidemment pour tout changement de seL4, il faut "refaire" les preuves!
        Et KataOS a modifié seL4 sans pour autant faire évoluer les preuves (pour le moment).

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.