OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 29 Март, 2024 01:48

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 17 ] 
Автор Сообщение
 Заголовок сообщения: Haskell и операционные системы
СообщениеДобавлено: Вторник, 18 Август, 2009 15:55 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Недавняя новость:

Австралийские ученые создали микроядро с формально подтвержденным уровнем защиты

Спрашивается, причём тут Хаскелл? История этого микроядра забавная -- сначала эти австралийцы сделали микроядро на Хаскелле, верифицировали, конвертировали вручную на Си, и вот, наконец, доказали, что их микроядро seL4 соответствует первоначальным исходникам на Хаскелле...
Кстати, эти исходники на Хаскелле также являются и документацией по микроядру (Running the Manual).

Ссылки по теме:

Secure Microkernel Project (seL4)
Open Kernel Labs and NICTA to Deliver Verified Microkernel / Hypervisor Technology to Mobile Market
Running the Manual: An Approach to High-Assurance. Microkernel Development


Последний раз редактировалось Geniepro Вторник, 18 Август, 2009 15:58, всего редактировалось 1 раз.

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Вторник, 18 Август, 2009 15:58 

Зарегистрирован: Вторник, 25 Апрель, 2006 16:21
Сообщения: 2180
Откуда: Нижний Новгород
Т.е. они, грубо говоря, спецификацию/Т.З. писали на хаскеле?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Вторник, 18 Август, 2009 16:02 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Почти. Точнее, на Literate Haskell, в котором главное -- комментарий (точнее, описание программы), и небольшие вкрапления хаскельного кода.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Вторник, 18 Август, 2009 16:33 

Зарегистрирован: Вторник, 25 Апрель, 2006 16:21
Сообщения: 2180
Откуда: Нижний Новгород
А как они верифицировали соответствия словесного описания тем вкраплениям кода?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Вторник, 18 Август, 2009 20:27 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Geniepro писал(а):
История этого микроядра забавная -- сначала эти австралийцы сделали микроядро на Хаскелле, верифицировали, конвертировали вручную на Си, и вот, наконец, доказали, что их микроядро seL4 соответствует первоначальным исходникам на Хаскелле...


Не трогая сам по себе Хаскелл...
Занятный пример якобы математики без понимания этой самой математики...
Мартышкин труд доказательства неизвестно чего неизвестно зачем.
Типа, волшебные формальные выкладки что-то там гарантируют.

Ещё раз нелишне повторить: доказать правильность = представить проверяемый объект в такой форме, в которой его правильность очевидна для любого специалиста непосредственной проверкой. Идеальный случай - "правильность по построению". Если не так, то применяются эквивалентные преобразования и какой-нибудь формализованный аппарат, но не заради самого по себе, а только в той мере, в какой он нужен.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Вторник, 18 Август, 2009 20:29 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Впрочем, не хочу сказать ничего дурного про этих австралийцев. Если им удобно так проверять свою работу - перекрёстной проверкой по двум эквивалентным формам, то на здоровье, хотя есть более короткие и надёжные пути.

Просто "вахи-охи" по этому поводу, как обычно, не про то :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Вторник, 18 Август, 2009 22:47 

Зарегистрирован: Вторник, 25 Апрель, 2006 16:21
Сообщения: 2180
Откуда: Нижний Новгород
Вообще, такое ощущение что они доказали правильность работы транслятора haskell->c для данного конкретного исходника.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 08:30 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Alexey Veselovsky писал(а):
Вообще, такое ощущение что они доказали правильность работы транслятора haskell->c для данного конкретного исходника.

Данный конкретный исходник транслировали люди, вот их работа и проверялась программой доказательства теорем.

Почитайте статью "Running the Manual", там описан их подход -- итеративный дизайн спецификации и реализации микроядра и его API, построение модели ядра на Хаскелле, выполнение его с некими прикладными программами на эмуляторе процессора, конвертирование хаскельного кода во входной язык системы доказательства теорем Isabelle с проверкой его свойств...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 08:35 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Илья Ермаков писал(а):
... есть более короткие и надёжные пути.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 08:39 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Чо-та я думал, что швейцарцы -- тёмный народ, ан нет:

Systems @ ETH Zurich, Haskell on the Metal

Как раз про эту seL4 упоминают, а так же про ещё парочку операционок на Хаскелле -- Osker и House. И если Osker -- микроядро, то House грузится с дискетки и даже примитивненький GUI с мышкой имеет...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 10:16 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Geniepro писал(а):
Не будет ли столь любезен многоуважаемый джин, что поведает нам об этих более коротких и надёжных путях, которые не являлись бы лишь частью того пути, который прошли эти австралийцы?

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

Потому что тех, кто понимает суть формальных методов, сама по себе мантра "мы формально доказали..." не убеждает.

Реальное доказательство свойств системы должно включать неформальное звено, ответственное за семантику. Это как раз самое слабое звено, и загромождение избыточной формалистикой его только затеняет.

Как будто что-то заоблачно трудное - написать безотказное ядро.

Суть обсуждаемых работ - возможность применения Хаскелла с некоторым формальным аппаратом для надёжного программирования. Т.е. исследование новых для Хаскелла вопросов. Но не новых вопросов для надёжного программирования. :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 10:25 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
К вопросу о безопасности.

Можно просто сформулировать такой базис операций, что изучение его свойств будет тривиальным. Вот в том и задача - выделить базис. Например, в "Эльбрусах" безопасность гарантирована контекстной организацией - сквозным и простым механизмом.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 11:25 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Geniepro писал(а):

Кстати, этот бритоголовый профессор Тимоти Роско, что ведёт данный проект в ETHZ, давно занимается подобной тематикой. В списке его публикаций значится, например, статья "Towards a practical, verified kernel" -- как раз про seL4. Роско как раз из команды этих австралийцев, переехал в ETHZ...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 16:08 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Safer software
Цитата:
The outcome is the result of four years’ research by Dr Klein’s team of 12 NICTA researchers, NICTA/UNSW PhD students and UNSW contributed staff. They successfully verified the C code and proved more than 10,000 intermediate theorems in more than 200,000 lines of formal proof. The proof is machine checked using the interactive theorem-proving program Isabelle. It is one of the largest machine-checked proofs ever done.
Да уж, 7500 строк на Си породили более 10 тыс. промежуточных теорем в более чем 200 тыс. строк этого доказательства.
Такой метод работы вряд ли приживётся в массовой разработке софта... :lol:


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 19:55 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
"Мышки плакали, давились, но продолжали кушать кактус".
Хотя сколько лет уже известно, что именно и как следует подразумевать под доказательной разработкой ПО.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 21:57 

Зарегистрирован: Четверг, 12 Июль, 2007 23:18
Сообщения: 1982
Откуда: Узбекистан, Чирчик
Илья Ермаков писал(а):
... нисходящее проектирование в сочетании с формулировкой логических предикатов и с опорой на строгий язык обеспечит не меньшую надёжность. Время, потраченное на переформализованную рутину, лучше потратить на хороший дизайн и проверку системы несколькими людьми.

А фактически они так и делали, только потом пошли дальше и сделали дополнительно и эту рутину. Видимо, их университет мог позволить себе такие траты ресурсов...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Haskell и операционные системы
СообщениеДобавлено: Среда, 19 Август, 2009 22:17 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
As pure science это вполне себе занятно, может быть :) И какой-то выход можно поиметь.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 17 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 0


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
cron
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2024, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB