Si ce genre de choses t'intéressent, tu peux aussi regarder le projet Bedrock; ce n'est pas présenté comme un OS, mais ça va quand même de l'assembleur à un petit serveur web, le tout entièrement vérifié (au niveau fonctionnel).
Ce qui est dommage c'est que la communauté Linux s'intéresse très peu à ces sujets-là. L'université (et l'armée) australienne a financé SeL4, Microsoft finance largement la recherche en méthodes formelles (le meilleur SMT solver vient chez eux, tout le monde s'en sert, mais il est propriétaire...), mais côté Linux, à part encourager mollement le travail sur Coccinelle et se plaindre des lint-like qui font trop de faux négatifs, il n'y a pas grand chose. Qui a essayé Cylone ou ATS ne serait-ce que 5 minutes, ou d'encoder des propriétés du kernel avec des descriptions ACSL?
[^] # Re: Virtualisation par défaut
Posté par gasche . En réponse à la dépêche Capsicum dans Linux : ça bouge !. Évalué à 4.
Si ce genre de choses t'intéressent, tu peux aussi regarder le projet Bedrock; ce n'est pas présenté comme un OS, mais ça va quand même de l'assembleur à un petit serveur web, le tout entièrement vérifié (au niveau fonctionnel).
Ce qui est dommage c'est que la communauté Linux s'intéresse très peu à ces sujets-là. L'université (et l'armée) australienne a financé SeL4, Microsoft finance largement la recherche en méthodes formelles (le meilleur SMT solver vient chez eux, tout le monde s'en sert, mais il est propriétaire...), mais côté Linux, à part encourager mollement le travail sur Coccinelle et se plaindre des lint-like qui font trop de faux négatifs, il n'y a pas grand chose. Qui a essayé Cylone ou ATS ne serait-ce que 5 minutes, ou d'encoder des propriétés du kernel avec des descriptions ACSL?