MirageOS - un micro OS (unikernel) en OCaml

• # coquille(s)

  Posté par Gil Cot ✔ (site web personnel, Mastodon) le 22 décembre 2021 à 19:12. Évalué à 2.

  

  Si la modération passe par là, il y a une étrange phrase à corriger :

  […] d’écrire quatre fois hello en 4quatresecondes et se termine.

  Merci pour cette dépêche intéressante.

  “It is seldom that liberty of any kind is lost all at once.” ― David Hume

  • [^] # Re: coquille(s)

    Posté par Pierre Jarillon (site web personnel) le 23 décembre 2021 à 01:00. Évalué à 3.

    

    Merci. Correction faite.

• # Intéressant

  Posté par Albirew (site web personnel, Mastodon) le 22 décembre 2021 à 21:12. Évalué à 6.

  

  En lisant le titre, je m'attendais à une nouvelle distro basée sur le même principe que hurd, mais en fait, ça à l'air de se rapprocher plus d'un OS comme alpine pour faire des containers (prévenez-moi si je me trompe)…

  EFBBBFE297AFE2978EE297AF0D0AE297AFE297AFE2978E0D0AE2978EE2978EE2978E

  • [^] # Re: Intéressant

    Posté par chimrod (site web personnel) le 22 décembre 2021 à 21:55. Évalué à 10.

    

    Il faut plutot le voir comme un cadriciel permettant de contruire "une application bootable". La librairie s’occupe de fournir les services bas-niveau (comme la pile tcp/ip présentée dans la dépeche) et permet de contruire une application dessus qui pourra etre exécutée dans un hyperviseur.

    Selon moi, le terme d’OS est inaproprié ici, car on s’est éloigné du logiciel permettant de lancer d’autres applications — encore que : cela est fait au moment de la compilation de l’image et non plus de l’exécution de l’OS comme on le retrouve habituellement. (si je voulais troller, je dirai que l’on pousse ici l’opposition entre langage interprété et langage compilé à l’extrème).

    Ça donne une idée de la quantité de travail nécessaire pour mettre en place la librairie, puisque le but est de fournir toutes les briques permettant de construire un système, non pas comme un gestionnaire de dépendance qui permet de construire son image, mais au sein d’une application unique.

• # Une petite mise à jour

  Posté par Dinosaure (site web personnel) le 24 décembre 2021 à 11:28. Évalué à 10. Dernière modification le 24 décembre 2021 à 11:28.

  

  Déjà je voudrais remercier les contributeurs qui ont continué d'écrire cette dépêche sans moi et c'est super cool! Merci à eux!

  Ensuite, j'aimerais juste continuer un petit peu cette dépêche en parlant de la prochaine release de MirageOS 4. En effet, si je n'ai pas pu prendre le temps de bien écrire cette dépêche dans le détail, c'est entre autre parce que nous étions occupé à préparer cette grosse release qui n'est toujours pas fini.

  Cependant, elle risque d'arrivé bientôt puisque nous avons presque enfin toutes les pièces réunis pour continuer notre support avec libseccomp, KVM (gcloud) et Xen. La nouvelle release nous permet d'étendre assez facilement nos cibles et nous avons commencer à proposer un MirageOS pour Raspberry Pi 4 (en bare-metal) - cela reste un proof-of-concept mais il permet de montrer que tout fonctionne correctement. Vous pouvez voir le projet ici: https://github.com/dinosaure/gilbraltar (et j'espère qu'il sera bientôt intégré à MirageOS).

  Ensuite, il est mention dans cette dépêche de tout un tas de librairies pour MirageOS. Encore une fois, ces librairies peuvent être utilisés en dehors de MirageOS - et c'est le cas. En parallèle de la release de MirageOS 4, nous avons continué à maintenir ces librairies pour les utilisateurs. À cela, on peut noter plusieurs avancés:
  - ocaml-dns va bientôt intégrer le support de DNSSEC (la PR)
  - mirage-crypto utilises une version vérifié (à l'aide de Coq) de certains algorithmes de cryptographies (l'article)
  - nous avons développé tout une "stack" pour les emails (envoie, réception et vérification) et nous avons désormais un relais SMTP (avec signature DKIM et vérification SPF/DMARC) (le projet)
  - irmin continue d'évoluer avec la crypto-monnaie Tezos (irmin)
  - un remplacement de la stack HTTP vient de s'opéré étant plus performant (plus de détail ici: le project)
  - enfin, nous nous préparons pour une migration vers OCaml multicore
  - et nous avons développé un OS qui permet de programmer une Guirlande en OCaml pour notre sapin :) (la photo et la vidéo)

  Bref, il y a là un énorme travail de fond pour une petite équipe (~10 personnes). Mais il est certains que si vous voulez jouer avec, nous aurions un plaisir de vous aider!

  • [^] # Re: Une petite mise à jour

    Posté par Ysabeau 🧶 🧦 (site web personnel, Mastodon) le 24 décembre 2021 à 11:55. Évalué à 7.

    

    Ben ça fera l'objet de la prochaine dépêche :-)

    Merci pour cette mise à jour.

    « Tak ne veut pas quʼon pense à lui, il veut quʼon pense », Terry Pratchett, Déraillé.

  • [^] # Re: Une petite mise à jour

    Posté par chimrod (site web personnel) le 28 décembre 2021 à 09:08. Évalué à 4.

    

    Merci pour les précisions !

    C’est super d’avoir une architecture physique comme le PI4 en cible ! Par contre, le pi4 est un peu overkill à mon niveau pour faire tourner MirageOS. Est-ce qu’il serait compliqué une fois cette première étape faite de l’étendre à d’autres modèles ? Le PI0v2 étant l’idéal (en terme de coût / consommation)

    C’est une bonne nouvelle également de passer sur httpaf plutôt que cohttp, qu’en est-il des webserver haut-niveau (opium / dream) ? Je vois qu’ils ne sont pas dans les paquets gérés sur le site de mirageOs, est-ce qu’il est possible de les compiler facilement dans l’architecture ?

    • [^] # Re: Une petite mise à jour

      Posté par Dinosaure (site web personnel) le 29 décembre 2021 à 00:02. Évalué à 5.

      

      RPi4 est en effet un peu "overkill". En vérité, ce dernier est plus un "proof of concept" de l'extensibilité de MirageOS sur d'autres architecture physique (comme ESP32, RISC-V, etc.). Le travail nécessaire pour étendre MirageOS à une autre "target" (et pouvoir ré-utiliser les libraires OCaml plus haut niveau comme HTTP ou DNS) est certes compliqué mais minimal! Pour revenir à RPi4, il nous a fallut que 4 jours pour ajouter la "target" à MirageOS et 3 semaines pour programmer notre guirlande.

      Les questions derrière ce travail concerne notamment la problématique de la cross-compilation notamment si une librairie tierce embarque du code C. Bref, tout ces aspects devraient être résolu et si on articule bien la séparation entre le micro-micro-kernel et le domaine applicatif, on devrait pouvoir réutiliser le même code pour Raspberry Pi Zero.

      Pour ce qui est de Dream, nous avons proposé cet été DreamOS et nous continuons à essayer de supporter Dream. Le développement de ce dernier est plus ou moins actif mais il devient de plus en plus nécessaire pour nous puisque nous essayons de créer un serveur Matrix avec MirageOS + Dream. Bref, de ce côté là aussi ça bouge :) !

• # Tous mes encouragements

  Posté par laparn le 29 décembre 2021 à 14:42. Évalué à 5.

  

  C'est ce que j'ai lu de plus intéressant sur un OS en 2021. C'est une approche très agressive, mais qui offre la perspective d'OS minimaux adaptés à une tâche unique. Et après tout, pour un projet donné (genre un serveur web, un serveur d'appli avec une bdd; ou un firewall; ou un serveur DNS ou de mail; ou un noeud de minage) on sent bien qu'il y a un paquet de trucs dans l'OS qui ne servent à rien et qui sont donc potentiellement autant de trous béants. Après, une approche "ocam-only" risque de limiter sérieusement les personnes à qui cela s'adresse. D'ailleurs, lire le peu de code dans l'article provoque pour un néophyte un certain malaise ("c'est quoi ce code ?"). En tout cas chapeau à l'équipe technique, réécrire une pile tcp-ip, tls, … c'est un sacré challenge.

  Typiquement, pour un serveur de vote électronique, c'est le genre de techno qui serait intéressante.

  • [^] # Re: Tous mes encouragements

    Posté par Ontologia (site web personnel) le 30 décembre 2021 à 01:30. Évalué à 3.

    

    C'est vrai qu'Ocaml a l'air d'un truc de matheux, mais on peu faire beaucoup de choses dans ce langage sans creuser toutes les geekeries matheuses que les caméliste adorent tricoter.

    module type ORDERED = sig
      type t
    
      val compare : t -> t -> int
    end
    
    module Make (S : ORDERED) : sig
      type 'a t
    
      val empty : 'a t
      val add : S.t -> 'a -> 'a t -> 'a t
    end

    On pourrait traduire ça en Java dans le genre (je peux me tromper attention)

    interface ORDERED<T> {
    
    int compare(a: T, b : T);
    
    }
    
    interface Make<ORDERED<T>, U<V>> {
     U<T> empty;
     U<V> add(e : T, a : V, b : U<V>);
    }

    « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

    • [^] # Re: Tous mes encouragements

      Posté par Gil Cot ✔ (site web personnel, Mastodon) le 30 décembre 2021 à 02:40. Évalué à 3.

      

      Mis côte à côte, comme tu fais, il n'y a pas de quoi faire peur et au contraire OCaml a l'air sympa.

      Bon, quand on regarde en détail, je préfère

      int compare(a: T, b : T);

      (les fonctions façon LISP… pour compare et add dans cet exemple) à

      val compare : t -> t -> int

      Inversement, je préfère de loin

      module Make (S : ORDERED) : sig
        …
      end

      à ce qui est de l'autre côté (exactement le même ressenti que j'ai avec Rust)

      interface Make<ORDERED<T>, U<V>> {
        …
      }

      Dans mon cas, c'est l'abus de symboles (surtout quand ça prend des sens divers selon les contextes –comme là délimiteur et ailleurs opérateurs booléens…) …pourtant j'ai fait de l'APL (oui assez vieux pour ça) et du J ainsi que du PERL…

      “It is seldom that liberty of any kind is lost all at once.” ― David Hume

      • [^] # Re: Tous mes encouragements

        Posté par kantien le 31 décembre 2021 à 00:23. Évalué à 5. Dernière modification le 31 décembre 2021 à 00:23.

        

        Bon, quand on regarde en détail, je préfère

        int compare(a: T, b : T);

        (les fonctions façon LISP… pour compare et add dans cet exemple) à

        val compare : t -> t -> int

        C'est une question de point de vue, et je trouve la syntaxe OCaml bien plus cohérente quand on la regarde dans l'ensemble du langage.

        Une expression de la forme val e : t se lit « e est une valeur de type t », et je ne vois pas pourquoi il faudrait changer de forme, sous prétexte que la valeur compare est ici une fonction. Le : de OCaml c'est comme le epsilon () des mathématiciens, il signifie l'appartenance à un ensemble. Ici, c'est l'ensemble des fonctions des t vers les fonctions des t dans les int (ça se lit t -> (t -> int)), c'est une fonction qui renvoie une fonction. De même, la fonction successeur sur les entiers a pour type int -> int, c'est une fonction des int vers les int.

        En résumé, on a donc un nom pour la valeur, suivi du : (le epsilon des matheux, ou le est du français comme dans « Socrate est un homme ») puis enfin une expression qui appartient au langage des types.

        Cette dernière expression, on pourrait la réutiliser telle quelle dans le langage des types, pour définir par exemple un type paramétrique, comme ici :

        type 'a comparator = 'a -> 'a -> int

        Ici comparator est une fonction des types dans les types (un type paramétrique) et 'a est le nom de son paramètre. On peut alors réécrire la signature du début ainsi:

        (* la fonction `comparator` appliquée au type `t` *)
        val compare : t comparator (* t -> t -> int *)

        Il y a en fait 4 langages dans OCaml :

        • le langage des valeurs et expressions
        • le langage des types des expressions
        • le langage des modules
        • le langage des types de modules ou signatures

        Les deux derniers, dont tu préfères la syntaxe, ont « globalement » les même principe syntaxiques que les deux premiers qui semblent te désarçonner. Pourquoi ?

        Pour le foncteur Make, on aurait pu écrire sa signature ainsi :

        module Make : functor (S : ORDERED) -> sig ... end

        ce qui est la même syntaxe que pour compare, à part le mot clef functor (personnellement, je le trouve inutile et j'aurais préféré qu'il soit absent, je trouve qu'il alourdit sans raison l'écriture et la lecture).

        Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

        • [^] # Re: Tous mes encouragements

          Posté par Gil Cot ✔ (site web personnel, Mastodon) le 31 décembre 2021 à 01:25. Évalué à 3. Dernière modification le 31 décembre 2021 à 01:27.

          

          et je ne vois pas pourquoi il faudrait changer de forme, sous prétexte que la valeur compare est ici une fonction. Le : de OCaml c'est comme le epsilon () des mathématiciens, il signifie l'appartenance à un ensemble.

          Pas faux :-) Je suis influencé par l'habitude visuelle des autres langages que je pratique plus souvent.

          C'est une question de point de vue, et je trouve la syntaxe OCaml bien plus cohérente quand on la regarde dans l'ensemble du langage.

          Une fois qu'on remet le nez dedans, OCaml est en effet plus cohérent ; c'est juste qu'il me faut chaque fois un peu de temps. (pas encore parfaitement multilingue.)

          “It is seldom that liberty of any kind is lost all at once.” ― David Hume

        • [^] # Re: Tous mes encouragements

          Posté par devnull80 le 14 janvier 2022 à 01:33. Évalué à 1.

          

          Je n'ai jamais aimé Caml à la fac, et ça continue.
          Cette syntaxe je ne la digère pas du tout, c'est juste incompréhensible pour mon esprit.

          Ton explication par exemple de :
          val compare : t -> (t -> int)

          Je me rappelle de mon prof qui disait qu'on pouvait le lire aussi:
          val compare : (t -> t) -> int

          Donc ça prend une fonction de t vers t et ça renvoie un int (qui de mon point de vue se rapproche davantage du "je prends 2 arguments et je renvoie un entier vrai/faux".
          À partir de là, s'il y a plusieurs niveaux de lecture, je laisse tomber.
          Ce langage est trop matheux à mon goût.
          Je ne pourrai jamais m'intéresser à un projet codé en (O)Caml, aussi intéressant puisse-t-il être.

          Mais merci pour ton explication, sans elle et son rappel de lecture, c'était le flou le plus total. Preuve que ce langage ne m'a pas marqué. Mais il suscite comme à l'époque une sorte d'énervement quand je le vois, je ne sais pas pourquoi …

          • [^] # Re: Tous mes encouragements

            Posté par kantien le 21 janvier 2022 à 10:56. Évalué à 4.

            

            Ce langage est trop matheux à mon goût.

            C'est une question de goût : personnellement, c'est pour cela que je l'aime. Un ordinateur, ça sert à calculer et tout ce qui s'éloigne, de près ou de loin, de la pratique mathématique en la matière, finit irrémédiablement à la poubelle chez moi. De plus, les mathématiciens, outre leur quête de rigueur, ont un penchant naturel pour une recherche d'esthétisme dans leur notation et la structure de leur discours : esthétisme que je ne retrouve pas dans les autres langages.

            Les mathématiques ont un triple but. Elles doivent fournir un instrument pour l’étude de la nature.

            Mais ce n’est pas tout : elles ont un but philosophique et, j’ose le dire, un but esthétique. Elles doivent aider le philosophe à approfondir les notions de nombre, d’espace, de temps.

            Et surtout leurs adeptes y trouvent des jouissances analogues à celles que donnent la peinture et la musique. Ils admirent la délicate harmonie des nombres et des formes ; ils s’émerveillent quand une découverte nouvelle leur ouvre une perspective inattendue ; et la joie qu’ils éprouvent ainsi n’a-t-elle pas le caractère esthétique, bien que les sens n’y prennent aucune part ? Peu de privilégiés sont appelés à la goûter pleinement, cela est vrai, mais n’est-ce pas ce qui arrive pour les arts les plus nobles ?

            Henri Poincaré, la valeur de la science

            Tu dois avoir des problèmes de souvenir sur ce que te disait ton prof.

            Ton explication par exemple de :
            val compare : t -> (t -> int)

            Je me rappelle de mon prof qui disait qu'on pouvait le lire aussi:
            val compare : (t -> t) -> int

            Donc ça prend une fonction de t vers t et ça renvoie un int (qui de mon point de vue se rapproche davantage du "je prends 2 arguments et je renvoie un entier vrai/faux".

            Je ne vois pas comment tu peux lire la seconde signature comme "je prends 2 arguments", alors qu'elle n'en prend qu'un qui est une fonction. De plus, on ne peut pas lire la première comme la seconde, mais celle-là est équivalente à une fonction avec cette signature :

            val compare : t * t -> int

            qui se lit déjà mieux comme "je prends 2 arguments…". Mais quand je dis qu'elles sont équivalentes, je ne veux pas dire que ce sont les mêmes, mais que je peux passer de l'une à l'autre et qu'elles calculeront la même chose. Le passage de l'une à l'autre se nomme curryfication mais ce n'est absolument pas propre à OCaml, comme l'illustre l'article de wikipédia. Ce passage de l'un à l'autre, ou cette équivalence, est identique à cette identité algébrique sur l'exponentielle et le produit :

            (A ^ B) ^ C = A ^ (B * C)
            

            L'exponentielle c'est le type des fonctions (la flèche -> lue de droite à gauche) et le produit c'est le produit cartésien sur les types (pour créer des paires).

            La version à la Curry permet de définir simplement des clôtures ou des applications partielles, comme dans cet exemple :

            List.map (compare 2) [1; 2; 3; 4; 5]

            D'ailleurs, au sens propre du terme, une fonction n'a toujours qu'un seul argument. Dans la version non curryfiée, il se trouve que cet unique argument est une paire (d'où la lecture "je prends 2 arguments…"), ce qu'il n'est pas dans la version à la Curry.

            En ce qui concerne, l'intérêt des fonctions qui retournent des fonctions (t -> (t -> int)) et des clôtures, tu pourras lire la discussion que l'on a eu récemment sur les génériques dans Go. Ici @wilk donne un lien vers un article qui, pour présenter la notion de clôture en Go, définit justement une fonction qui retourne une fonction.

            Je ne pourrai jamais m'intéresser à un projet codé en (O)Caml, aussi intéressant puisse-t-il être.

            Je n'aime pas l'ananas mais je crois, qu'ici, tout le monde s'en fout, et je ne vois pas bien l'intérêt d'exprimer la chose publiquement. Dans le cas présent, je doute que les auteurs du projet puissent être, pour leur part, intéresser pas les contributions que tu pourrais apporter.

            Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

  • [^] # Re: Tous mes encouragements

    Posté par kantien le 28 janvier 2022 à 12:06. Évalué à 4.

    

    Typiquement, pour un serveur de vote électronique, c'est le genre de techno qui serait intéressante.

    D'autant qu'il existe un système de vote électronique à l'état de l'art en OCaml : Belenios. Il a été présenté sur le blog de vulgarisation de la Société Informatique de France, (a voté) Euh non : a cliqué.

    C'est ce que j'ai lu de plus intéressant sur un OS en 2021.

    Si le sujet t'intéresse, il y a une interview d'Anil Madhavapeddy, le créateur de MirageOS, sur le thème What is an operating system ? Où l'on y apprend entre autre que l'hyperviseur Xen est né d'un pari dans un pub de Cambridge (la bière anglaise donne des idées) et que la première version de MirageOS servait à tester les couches bas niveau de Xen.

    À titre personnel, un des passages qui m'a bien plu sur le choix du langage :

    And OCaml, in my mind, is a generational language. One of the properties I want from systems I build is that they last the test of time. It’s so frustrating that a system I built in the early 2000s, if you put it on the internet today, would be hacked in seconds. It just would not survive for any length of time. So how do we even begin the discipline of building systems that can last for, forget a decade, just even a year without having some kind of security holes or some kind of terrible, terrible flaw?

    Now, there is one argument saying that you should build living systems that are perpetually refreshed but also we should have the hope of building eternal systems that have beautiful mathematical properties and still perform useful, utilitarian functions in the world.

    Passage immédiatement suivi par cette question de Yaron Minsky :

    There’s one big downside I feel like I see in all of this which you haven’t talked about yet which is it requires you to write all of your code in OCaml. And I really like OCaml, you really like OCaml, it’s in some sense not a downside, but if you’re trying to build software that’s broadly useful and usable and can build a big ecosystem around it, restricting down to one particular programming language can be awkward.

    Just to say the obvious, I would find it somewhat awkward if there’s some operating system I wanted to use and I had to use whatever their favorite language was and I couldn’t write in my favorite language. How do you think about this trade off?

    lire la suite :-)

    Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

• # Quid du debugging ?

  Posté par Firwen (site web personnel) le 24 janvier 2022 à 19:23. Évalué à 10.

  

  Si je trouve le concept d'Unikernel intéressant sur de la virtualisation pour toute une série de raison:

  • diminuer l'emprunte en terme de ressources
  • minimiser la surface d'attaque
  • facilite le lifecycle de l'App
  • etc

  Il y a un aspect qui m'a toujours bloque d'utiliser ça en production: Le debugging et profiling:

  Simple curiosité: Qu'est ce que vous avez pour ça sous MirageOS par exemple ?

  Sous Linux, je peux toujours compter sur GDB, perf, strace, l'OOM killer, les coredumps, les logs systems, etc.

  Dans le cas d'un unikernel ? est-ce qu'il y a un tooling existant excepté la botte et le couteau ?

• # Commentaire supprimé

  Posté par sophiaabigail le 27 janvier 2022 à 07:58. Évalué à 0. Dernière modification le 27 janvier 2022 à 08:17.

  

  Ce commentaire a été supprimé par l’équipe de modération.

Suivre le flux des commentaires

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