LINUX.ORG.RU

Открыты исходники seL4!

 ,


7

5

General Dynamics C4 Systems и NICTA рады объявить об открытии исходных кодов seL4 — первого в мире ядра операционной системы с доказанной корректностью:

  • бинарный код микроядра seL4 правильно реализует поведение, описанное в его абстрактной спецификации;
  • данные не могут быть изменены либо прочитаны без разрешения;
  • ранее, в 2009 году, разработчиками было доказано соответствие исходного кода ядра, написанного на языке Си, и его спецификации. Теперь же дополнительно показана двоичная корректность.

Исходные коды доступны для широкой публики на GitHub.

>>> Подробности

★★★★★

Проверено: fallout4all ()

Внесите царя, хотелось бы услышать его авторитетное мнение по этому поводу.

ymn ★★★★★ ()

ранее, в 2009 году, разработчиками было доказано соответствие исходного кода ядра, написанного на языке Си, и его спецификации. Теперь же дополнительно показана двоичная корректность.

Вот, в то время, как Линус Трольвальдс исходит говном по поводу бага в GCC, эти специалисты тихо и незаметно всё решают. А потом это никому не нужно, потому что видеокарты от невидии не поддерживаются.

proud_anon ★★★★★ ()
Ответ на: комментарий от ymn

Ну и это явно не для широкого применения, по крайней мере пока.

Так шутка же. Но с долей правды. Как только этим ребятам понадобится какая-нибудь CUDA...

proud_anon ★★★★★ ()
Последнее исправление: proud_anon (всего исправлений: 1)

Во-первых хорошо, что разработка новых операционных систем ведется и не стоит на месте. Используемые сегодня имеют кучу проблем, которые надо решать.

Во-вторых какие у него интефейсы для модулей? Это ведь не posix насколько я понял?

loz ★★★★★ ()
Ответ на: комментарий от proud_anon

Как только этим ребятам понадобится какая-нибудь CUDA

Они попросят других ребят запилить им дрова

buddhist ★★★★★ ()
Ответ на: комментарий от ymn

А КАК ВЫ ДОКАЖИТИ КОРЕКТНОСТЬ ПРОВЕРЯТИЛЯ КОРЕКТНОСТИ?!?!?!

А так, конечно, очень впечатляющая новость. Но что такое Isabelle (в тегах)?

CARS ★★★★ ()

! в заголовке говорит, что все должны испытывать эйфорию по поводу данного события?

vitalif ★★★★★ ()

4.2

первого в мире ядра операционной системы с доказанной корректностью

Доказана не корректность ядра, но соответствие спецификации. Какие дыры в спецификации пока неизвестно.

Camel ★★★★★ ()
Ответ на: комментарий от sehellion

Это микроядро, модель которого была реализована на Haskell и формально верифицирована. А нужно оно для чего угодно. Хоть новую ОС лепи, хоть гипервизор на его основе (именно это уже сделано, если мне не изменяет память).

happycorsair ()

первого в мире ядра операционной системы с доказанной корректностью:

Hello_world без ошибок выводит?

devl547 ★★★★★ ()
Ответ на: комментарий от CARS

The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC). Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification. Though interactive, Isabelle also features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. The Isabelle theorem prover is free software, released under the revised BSD license.

ymn ★★★★★ ()
Ответ на: 4.2 от Camel

Доказана не корректность ядра, но соответствие спецификации

Разумеется. Формальная верификация занимается исключительно этим.

ymn ★★★★★ ()
Ответ на: комментарий от vitalif

Да. Это довольно популярная в узких кругах саксесс стори.

ymn ★★★★★ ()

там кода кот наплакал. читается очень хорошо, для обучения может сгодится, но мега функциональных возможностей я не увидел. И оно вроде как не реалтайм. В общем, для любого реального применения там пилить и пилить.

vtVitus ★★★★★ ()
Последнее исправление: vtVitus (всего исправлений: 1)

Лицензия какая?

А под какой лицензией открыты исходники? В репозитарии выложены GPLv2 и BSD, которые между собой не совместимы.

Camel ★★★★★ ()
Ответ на: комментарий от anonymous

:) Ну вот, всё нормально, а я уж было перепугался, как так.

yoghurt ★★★★★ ()
Ответ на: комментарий от goingUp

Внезапно. А всё началось со смены опроса на главной...

Xellos ★★★★★ ()

Вроде годно, потыкаем на досуге

anonymous ()
Ответ на: комментарий от Indexator

Это негодный анон. Игнорируй его. Хотя ты регистрантишка, ты не умеешь игнорировать.

anonymous ()

Ну всё, теперь математики горе-погромиздов, не могущих корректно работающий код без тестирования написать, заклюют.

MiniRoboDancer ★☆ ()
Ответ на: комментарий от Deleted

Нельзя требовать

BSD совместима с GPL, но не наоборот

BSD требует указывать авторство, GPL запрещает добавлять требования момимо тех что имеются в GPL. BSD и GPL несовместмимы.

Думаете почему код из Linux'а не попадает в ядро FreeBSD и наоборот?

Camel ★★★★★ ()
Последнее исправление: Camel (всего исправлений: 1)

ранее, в 2009 году, разработчиками было доказано соответствие исходного кода ядра, написанного на языке Си, и его спецификации.

Но потом его собрали при помощи gcc-4.9.0...

atrus ★★★★★ ()
Ответ на: Нельзя требовать от Camel

Re: Нельзя требовать

Потому что попадает. BSD совместима с GPLv2, то есть код под BSD можно взять и перелицензировать под GPLv2, что было проделано с кодом из OpenBSD(Тео тогда еще гору кирпичей отложил), а вот в обратную сторону совместимости нет, по этой причине в FreeBSD никогда не будет нормального кода. Ну и да, авторы могут хоть 100 лицензий сразу навешивать на свой код, в таких случаях можно выбирать под какой он для тебя, а не визжать, что они несовместимы.

anonymous ()
Ответ на: Нельзя требовать от Camel

Re: Нельзя требовать

Думаете почему код из Linux'а не попадает в ядро FreeBSD и наоборот?

Код из Linux'а таки попадает в xBSD, только этот код не под GPL. Наоборот тоже бывает.

hateyoufeel ★★★★★ ()
Ответ на: Нельзя требовать от Camel

А да, бсд... «When you want to refer specifically to one of the BSD licenses, please always state which one: the “original BSD license” or the “revised BSD license”.»

Однако на гитхабе лежит LICENSE_BSD2.txt - это 2-clause BSD. Совместима с GPL. http://en.wikipedia.org/wiki/BSD_licenses

Deleted ()
Ответ на: Re: Нельзя требовать от anonymous

Нельзя

код под BSD можно взять и перелицензировать под GPLv2

Нельзя. Однажды BSD — всегда BSD. BSD разрешает делать всё что угодно, но требует указывать что используется код опубликованый под лицензией BSD. В GPL нет такого требования, а дополнительные требования GPL добавлять запрещает.

Camel ★★★★★ ()
Ответ на: Нельзя от Camel

документальное подтверждение твоим словам, пожалуйста

Deleted ()
Ответ на: комментарий от MiniRoboDancer

Ну и зачем такое самоистязание (написание кода без тестов), когда можно сразу описать спецификацию через BDD и код можно будет писать хоть в пьяном угаре с перерывом на шлюх и кокаин, а тесты будут постоянно держать разрабов в заранее определенном коридоре спецификации?

Indexator ★★★ ()
Ответ на: комментарий от Indexator

можно сразу описать спецификацию через BDD и код можно будет писать хоть в пьяном угаре с перерывом на шлюх и кокаин, а тесты будут постоянно держать разрабов в заранее определенном коридоре спецификации?

А вот и наркоманы подтянулись...

tailgunner ★★★★★ ()
Ответ на: Нельзя от Camel

Re: Нельзя

Бред. BSDL на то и BSDL, что лицензию его форка можно менять — перелицензировать под какой-нибудь Apache или GPL, а то и вовсе запроприетарить (чем активно пользуется сонька).

anonymous ()

Аксиома: «В каждой программе есть хотя бы одна „ашипка“» :)

quickquest ★★★★★ ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.