| OberonCore https://forum.oberoncore.ru/ |
|
| Haskell и операционные системы https://forum.oberoncore.ru/viewtopic.php?f=72&t=1771 |
Страница 1 из 1 |
| Автор: | Geniepro [ Вторник, 18 Август, 2009 15:55 ] |
| Заголовок сообщения: | Haskell и операционные системы |
Недавняя новость: Австралийские ученые создали микроядро с формально подтвержденным уровнем защиты Спрашивается, причём тут Хаскелл? История этого микроядра забавная -- сначала эти австралийцы сделали микроядро на Хаскелле, верифицировали, конвертировали вручную на Си, и вот, наконец, доказали, что их микроядро 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 |
|
| Автор: | Alexey Veselovsky [ Вторник, 18 Август, 2009 15:58 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Т.е. они, грубо говоря, спецификацию/Т.З. писали на хаскеле? |
|
| Автор: | Geniepro [ Вторник, 18 Август, 2009 16:02 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Почти. Точнее, на Literate Haskell, в котором главное -- комментарий (точнее, описание программы), и небольшие вкрапления хаскельного кода. |
|
| Автор: | Alexey Veselovsky [ Вторник, 18 Август, 2009 16:33 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
А как они верифицировали соответствия словесного описания тем вкраплениям кода? |
|
| Автор: | Илья Ермаков [ Вторник, 18 Август, 2009 20:27 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Geniepro писал(а): История этого микроядра забавная -- сначала эти австралийцы сделали микроядро на Хаскелле, верифицировали, конвертировали вручную на Си, и вот, наконец, доказали, что их микроядро seL4 соответствует первоначальным исходникам на Хаскелле... Не трогая сам по себе Хаскелл... Занятный пример якобы математики без понимания этой самой математики... Мартышкин труд доказательства неизвестно чего неизвестно зачем. Типа, волшебные формальные выкладки что-то там гарантируют. Ещё раз нелишне повторить: доказать правильность = представить проверяемый объект в такой форме, в которой его правильность очевидна для любого специалиста непосредственной проверкой. Идеальный случай - "правильность по построению". Если не так, то применяются эквивалентные преобразования и какой-нибудь формализованный аппарат, но не заради самого по себе, а только в той мере, в какой он нужен. |
|
| Автор: | Илья Ермаков [ Вторник, 18 Август, 2009 20:29 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Впрочем, не хочу сказать ничего дурного про этих австралийцев. Если им удобно так проверять свою работу - перекрёстной проверкой по двум эквивалентным формам, то на здоровье, хотя есть более короткие и надёжные пути. Просто "вахи-охи" по этому поводу, как обычно, не про то 
|
|
| Автор: | Alexey Veselovsky [ Вторник, 18 Август, 2009 22:47 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Вообще, такое ощущение что они доказали правильность работы транслятора haskell->c для данного конкретного исходника. |
|
| Автор: | Geniepro [ Среда, 19 Август, 2009 08:30 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Alexey Veselovsky писал(а): Вообще, такое ощущение что они доказали правильность работы транслятора haskell->c для данного конкретного исходника. Данный конкретный исходник транслировали люди, вот их работа и проверялась программой доказательства теорем. Почитайте статью "Running the Manual", там описан их подход -- итеративный дизайн спецификации и реализации микроядра и его API, построение модели ядра на Хаскелле, выполнение его с некими прикладными программами на эмуляторе процессора, конвертирование хаскельного кода во входной язык системы доказательства теорем Isabelle с проверкой его свойств... |
|
| Автор: | Geniepro [ Среда, 19 Август, 2009 08:35 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Илья Ермаков писал(а): ... есть более короткие и надёжные пути. Не будет ли столь любезен многоуважаемый джин, что поведает нам об этих более коротких и надёжных путях, которые не являлись бы лишь частью того пути, который прошли эти австралийцы? Есть ли у Вас реальные примеры подобных работ без применения формальных методов, но с не менее надёжными результатами? И почему эти примеры (если они есть) так малоизвестны? |
|
| Автор: | Geniepro [ Среда, 19 Август, 2009 08:39 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Чо-та я думал, что швейцарцы -- тёмный народ, ан нет: Systems @ ETH Zurich, Haskell on the Metal Как раз про эту seL4 упоминают, а так же про ещё парочку операционок на Хаскелле -- Osker и House. И если Osker -- микроядро, то House грузится с дискетки и даже примитивненький GUI с мышкой имеет... |
|
| Автор: | Илья Ермаков [ Среда, 19 Август, 2009 10:16 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Geniepro писал(а): Не будет ли столь любезен многоуважаемый джин, что поведает нам об этих более коротких и надёжных путях, которые не являлись бы лишь частью того пути, который прошли эти австралийцы? Уважаемый Джин-Про не хуже меня знает, что нисходящее проектирование в сочетании с формулировкой логических предикатов и с опорой на строгий язык обеспечит не меньшую надёжность. Время, потраченное на переформализованную рутину, лучше потратить на хороший дизайн и проверку системы несколькими людьми. Потому что тех, кто понимает суть формальных методов, сама по себе мантра "мы формально доказали..." не убеждает. Реальное доказательство свойств системы должно включать неформальное звено, ответственное за семантику. Это как раз самое слабое звено, и загромождение избыточной формалистикой его только затеняет. Как будто что-то заоблачно трудное - написать безотказное ядро. Суть обсуждаемых работ - возможность применения Хаскелла с некоторым формальным аппаратом для надёжного программирования. Т.е. исследование новых для Хаскелла вопросов. Но не новых вопросов для надёжного программирования.
|
|
| Автор: | Илья Ермаков [ Среда, 19 Август, 2009 10:25 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
К вопросу о безопасности. Можно просто сформулировать такой базис операций, что изучение его свойств будет тривиальным. Вот в том и задача - выделить базис. Например, в "Эльбрусах" безопасность гарантирована контекстной организацией - сквозным и простым механизмом. |
|
| Автор: | Geniepro [ Среда, 19 Август, 2009 11:25 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Geniepro писал(а): Кстати, этот бритоголовый профессор Тимоти Роско, что ведёт данный проект в ETHZ, давно занимается подобной тематикой. В списке его публикаций значится, например, статья "Towards a practical, verified kernel" -- как раз про seL4. Роско как раз из команды этих австралийцев, переехал в ETHZ... |
|
| Автор: | Geniepro [ Среда, 19 Август, 2009 16:08 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
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 тыс. строк этого доказательства.Такой метод работы вряд ли приживётся в массовой разработке софта... 
|
|
| Автор: | Илья Ермаков [ Среда, 19 Август, 2009 19:55 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
"Мышки плакали, давились, но продолжали кушать кактус". Хотя сколько лет уже известно, что именно и как следует подразумевать под доказательной разработкой ПО. |
|
| Автор: | Geniepro [ Среда, 19 Август, 2009 21:57 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
Илья Ермаков писал(а): ... нисходящее проектирование в сочетании с формулировкой логических предикатов и с опорой на строгий язык обеспечит не меньшую надёжность. Время, потраченное на переформализованную рутину, лучше потратить на хороший дизайн и проверку системы несколькими людьми. А фактически они так и делали, только потом пошли дальше и сделали дополнительно и эту рутину. Видимо, их университет мог позволить себе такие траты ресурсов... |
|
| Автор: | Илья Ермаков [ Среда, 19 Август, 2009 22:17 ] |
| Заголовок сообщения: | Re: Haskell и операционные системы |
As pure science это вполне себе занятно, может быть И какой-то выход можно поиметь.
|
|
| Страница 1 из 1 | Часовой пояс: UTC + 3 часа |
| Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |
|