The OpenNET Project / Index page

[ новости /+++ | форум | теги | ]

Проекту seL4 присуждена премия ACM Software System Award

06.05.2023 21:58

Проект, развивающий открытое микроядро seL4, получил премию ACM Software System Award, ежегодно присуждаемую Ассоциация вычислительной техники (ACM), наиболее авторитетной международной организации в области компьютерных систем. Премия присуждена за достижения в области математического доказательства надёжности работы, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям и признаёт готовность использования в критически важных применениях. Проект seL4 показал, что можно не только полностью провести формальную верификацию надёжности и безопасности для проектов уровня промышленных операционных систем, но и добиться этого без ущерба производительности и универсальности.

Награда ACM Software System Award ежегодно вручается за разработку программных систем, оказавших определяющее влияние на отрасль, внеся в обиход новые концепции или раскрывших новые области коммерческого применения. Размер премии 35 тысяч долларов США. В прошлые годы премии ACM были присуждены проектам GCC и LLVM, и их основателям Ричарду Столлману и Крису Латнеру. Премией также были отмечены такие проекты и технологии, как UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB и Eclipse.

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

  1. Главная ссылка к новости (https://www.acm.org/media-cent...)
  2. OpenNews: Проект Neptune OS развивает слой совместимости с Windows на базе микроядра seL4
  3. OpenNews: Микроядро seL4 математически верифицировано для архитектуры RISC-V
  4. OpenNews: Открыт код сверхнадёжного микроядра seL4
  5. OpenNews: На базе гипервизора seL4 создана платформа для создания высокозащищённых систем
  6. OpenNews: Проекту LLVM присуждена премия ACM Software System Award
Лицензия: CC BY 3.0
Короткая ссылка: https://opennet.ru/59091-sel4
Ключевые слова: sel4
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (49) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, Аноним (1), 22:34, 06/05/2023 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Скоро Фуксия со своим Цирконом спустится и покроет всё стадо.
     
     
  • 2.3, пох. (?), 22:38, 06/05/2023 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Угу, спустится, с высот фоторамки и что там еще - говорящий кофейник?

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

    В принципе, конечно, от sel4 тоже толку никакого, занятный но феерично ненужный артефакт.

     
     
  • 3.5, Аноним (1), 23:11, 06/05/2023 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Про джаву тоже говорили что он только для кофемашин. И где сейчас джава? Да она везде, бро!
     
     
  • 4.36, _ (??), 04:15, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    Ну да - на всех кладбищах (enterprise environment). Новых проектов на ней нет. Как и предсказывалось - новый Кобол :(
     
     
  • 5.38, Аноним (38), 08:49, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Ксожалению, таки есть. Для новых прозектов берут Швинг и продолжают пейсать на джяве. И логика в этом есть, и есть причины так делать.
     
     
  • 6.39, Аноним (39), 11:20, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +1 +/
    А чем Котлин не джава?
     
  • 5.63, Аноним (63), 21:00, 11/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    > на всех кладбищах (enterprise environment)

    Однако эти "кладбища" почему-то способны платить тебе стабильную хорошую ЗП, в отличие от "новых проектов" твоего одноклассника Васяна на модных язычках, от которых писаются кипятком все пацаны на раёне

     
  • 4.40, Заноним (?), 18:51, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    Да не везде, и вообще она давно закатывается. И даже graalvm её не вытянет.
    Как ранее сказали - очередной cobol.
     
     
  • 5.64, Аноним (63), 21:01, 11/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    Мне нравятся такие "древние" языки.
    Чем меньше дешёвой школоты хочет с ней работать - тем больше моя ЗП
     
     
  • 6.65, Заноним (?), 00:28, 12/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    Ну на java столько понаписали, что ЗП ещё долго будут платить.
     
  • 2.43, Аноним (43), 21:36, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Скоро Фуксия

    у гугла и на sel4 есть ОС

    https://www.opennet.ru/opennews/art.shtml?num=57920

     

  • 1.6, Анонн (?), 23:20, 06/05/2023 [ответить] [﹢﹢﹢] [ · · · ]  
  • +7 +/
    Очень крутой проект, показывающий насколько тяжело и дорого так разрабатывать софт.
    Там всего меньше 10к строк кода ("8,700 lines of C code and 600 lines of assemble" если быть точным).

    При этом "затраты" на аналогичную верификацию при уже проработанной методологии - 8 (восемь) человеко-лет ("kernel plus proof of 8 py")

    В процессе верификации пришлось писать кучу уточнений,
    нашли 16 дефектов до второй фазы верификации, сама формальная верификация нашла 144 дефекта и необходимость внести 54 изменения. Т.е. где-то 1 дефект на 50 строк си/асм кода.

    Подробности тут: https://www.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf

     
     
  • 2.7, Аноним (1), 23:29, 06/05/2023 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Поэтому Hurd и не смогли дописать.
     
     
  • 3.10, пох. (?), 00:10, 07/05/2023 [^] [^^] [^^^] [ответить]  
  • –2 +/
    Нет, его к счастью писали, а не верифицировали-верифицировали.

    Просто на фоне линукса это неповоротливое чудовище (с драйверами, как нельзя более кстати, копипащенными из линукса же) оказалось никому совершенно не нужным.

    Т.е. добились что оно загружалось и можно было даже набрать /bin/ls - но что делать дальше все равно никто не знал.

    А это недоразумение даже и такого не может.

     
  • 2.8, vitalif (ok), 23:32, 06/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    в этом контексте "для проектов уровня промышленных операционных систем" звучит слегка забавно
     
     
  • 3.45, пох. (?), 23:09, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    промышленная - это в промышленности. Каким-нибудь приводом конвейера управлять, с положением на две позиции - заготовка едет и заготовка стоит.

    Или еще что незамысловатое. Тут верю, вполне годится. Ну если pic какой слишком сложно этим озадачить.

     
  • 2.22, Аноним (22), 08:33, 07/05/2023 [^] [^^] [^^^] [ответить]  
  • –1 +/
    верификация

    Слово "проверка" ведь с более меньшим углеродным следом, товарищи.. )

     
     
  • 3.41, Аноним (41), 19:24, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +5 +/
    Верификация - проверка
    Аутентификация - проверка
    Авторизация - проверка
    Валидация - проверка
     
  • 2.42, warlock66613 (ok), 20:58, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    Интересные подробности. Я особенно обратил бы внимание на то, что 1) это всё пока без поддержки многоядерности/мультипроцессорности, 2) им пришлось жёстко отказаться от указателей на стек: если в коде указатель, то его цель — в куче. Довольно серьёзные ограничения, особенно если подумать о них вместе.
     

  • 1.9, InuYasha (??), 23:37, 06/05/2023 Скрыто ботом-модератором [﹢﹢﹢] [ · · · ]     [к модератору]
  • –1 +/
     

     ....ответы скрыты (7)

  • 1.24, Аноним (24), 08:54, 07/05/2023 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Они что-то там на Haskell начудили, молодцы.

    А я могу таким же образом мой код верифицировать?

    У меня есть несколько крошечных проектов, на тысячу строк.

     
     
  • 2.61, warlock66613 (ok), 12:16, 10/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    Нет. Вы же наверняка используете сторонние библиотеки, как минимум стандартную библиотеку.
     

  • 1.29, Аноним (29), 12:48, 07/05/2023 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > вручается за разработку программных систем, оказавших определяющее влияние на отрасль

    шта?! А можно чуть подробнее, на что повлияла разработка seL4? Может, какие-то ОС на ней написали годные? Хотя бы уровня Линукса - 1% декстопа и то хорошо. Или seL4 только тем и хороша, что про неё ГОДАМИ только и можно писать, что она "верифицируемая"? :))))))) (проверяемая, клоуны!)

     
     
  • 2.31, Аноним (31), 13:47, 07/05/2023 [^] [^^] [^^^] [ответить]  
  • –1 +/
    https://www.opennet.ru/opennews/art.shtml?num=59052
    Это Вам не подойдет?
     
  • 2.32, пох. (?), 16:34, 07/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    > А можно чуть подробнее, на что повлияла разработка seL4?

    "Болгары восхитились!"

    Ну и вообще, чего докопался, это не троллейбус из буханки, это корабль в бутылке в форме буханки. Кросивое!  Поставить в музей на центральное место экспозиции, ходить вокруг на цыпочках, умиляться. Потом, когда-нибудь, обнаружим что интел впилил ее в ядро своего ME заместо нынешнего (тоже троллейбуса но гораздо менее выдающегося) или еще где в подобном месте всплывет.

    > (проверяемая, клоуны!)

    этому - десять плетей за иноземные слова воспрещенные.
    Не клоуны, а скоморохи!

    Клоуны - это когда в DF докопался до адамантина на один лишний кубик.

     
  • 2.33, Степан (?), 19:02, 07/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    > декстопа
    > проверяемая, клоуны
     
     
  • 3.35, пох. (?), 21:54, 07/05/2023 [^] [^^] [^^^] [ответить]  
  • +1 +/
    О, точно, двадцать плетей басурманину! Столешница, скоморох!

     
  • 2.44, Аноним (43), 21:47, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > на что повлияла разработка seL4?

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

    https://en.wikipedia.org/wiki/PikeOS

     
     
  • 3.46, пох. (?), 23:17, 08/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    чегой-то мне кажется что мэйнстрим сейчас - как в тойете с педалью газа. Когда при наличии двухканального датчика индус ляпает еще один китайский глючный (потому что не знает про второй канал или не умеет вообще в тот датчик) а потом кодит такое что счастливый клиент убивается апстену. Всем похрену.

    https://en.wikipedia.org/wiki/PikeOS
    It enables users to build certifiable smart devices for the Internet of things (IoT)

    Т.е. и этим прекрасным микроскопом просто забивают гвозди.
    Ну в общем логично, учитывая eclipse и прочий трэшачок.

     
     
  • 4.47, Аноним (43), 10:27, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    > мне кажется что мэйнстрим сейчас - как в тойете с педалью газа

    майнстрим сейчас исключить человеческий фактор из управления автомобилями

    https://www.mobileye.com/

    > Т.е. и этим прекрасным микроскопом просто забивают гвозди

    они зарабатывают на всём, денег больше всего в ширпотребе. В автомобилях выпускаемых в Германии используют открытый фреймворк l4re

    https://www.kernkonzept.com

     
     
  • 5.48, пох. (?), 11:28, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    Ну вот тойета опередила тренд на десять лет. Правда, "исключенному" человеческому фактору кажется не очень понравилось вляпываться в стену.

     
  • 5.49, Аноним (49), 12:37, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > майнстрим сейчас исключить человеческий фактор из управления автомобилями
    > https://www.mobileye.com/

    Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.
    Маск вон, уже почти десять лет - "еще немного и уже почти совсем скоро" и ниче, пипл хавает за обе щеки.

    А в реальности, хорошо если лет через 15-20 что-то не сильно стремное в этой области появится.

     
     
  • 6.52, пох. (?), 15:24, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    Ну зочем вы тгавите - Маск всего двух только пока и убил. (Ну трех если считать отправленного в космос с билетом в один конец)
     
  • 6.54, Аноним (43), 16:25, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    > Майстрим сейчас, как и всегда - подоить доверчивых лошк^W инвесторов и потребляd^Hтелей.

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

     
     
  • 7.55, Аноним (49), 17:16, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    А в огороде бузина, это тоже очевидно Внезапно, можно развивать технологии и пр... большой текст свёрнут, показать
     
     
  • 8.59, Аноним (43), 23:28, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • +/
    внезапно переход от L2 к L3 имеет чисто правовые сложности - после сертификации ... текст свёрнут, показать
     
     
  • 9.60, Аноним (49), 11:37, 10/05/2023 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Угу, чисто правовые сложности опять танцорам мешают, а не то они бы всем показ... большой текст свёрнут, показать
     
     
  • 10.62, Аноним (43), 09:31, 11/05/2023 [^] [^^] [^^^] [ответить]  
  • –1 +/
    сказки не надо рассказывать - когда там всплеск развития ИИ начался несколько ... текст свёрнут, показать
     
  • 4.51, Аноним (51), 14:04, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • –2 +/
    с моей точки зрения вся эта идея формальной верификации микроядра и полученной з... большой текст свёрнут, показать
     
     
  • 5.53, пох. (?), 15:26, 09/05/2023 [^] [^^] [^^^] [ответить]  
  • +1 +/
    поток сознания эксперта опеннета

    Про то что такое формальная верификация и как это работает - читать ему разумеется, не интересно и незачем, у него уже есть ценное мнение.

     

  • 1.34, fidoman (ok), 19:45, 07/05/2023 [ответить] [﹢﹢﹢] [ · · · ]  
  • –2 +/
    Строгое математическое доказательство показало, что все предусмотренные ТЗ бекдоры на месте.
     
  • 1.50, Аноним (51), 14:03, 09/05/2023 [ответить] [﹢﹢﹢] [ · · · ]  
  • –4 +/
    лично мне чужды подобные инновационные решения встроеных систем, я предпочитаю разрабатывать прикладные решения на языке си-плюсплюс в среде майкрософт визуал студио, а для моих задач со средней нагрузкой предпочтительнее простой монолитный ядренной архитектуры виндовс,которая проверенная временем и хорошо изученная, а эти "легковесные" микроядра только усложняют работу без очевидных преимуществ для обычного прикладного разработчика,как говорится "если не сломалось - не чини" и кто то явно преувеличивает значимость этого проекта чтобы получить гранты и деньги, поэтому я не вижу ничего выдающегося в этом проекте и его награждении
     

     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Партнёры:
    PostgresPro
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

    Закладки на сайте
    Проследить за страницей
    Created 1996-2024 by Maxim Chirkov
    Добавить, Поддержать, Вебмастеру