OberonCore https://forum.oberoncore.ru/ |
|
OS Day 2020 https://forum.oberoncore.ru/viewtopic.php?f=6&t=6671 |
Страница 2 из 2 |
Автор: | Иван Денисов [ Вторник, 02 Февраль, 2021 16:14 ] |
Заголовок сообщения: | Re: OS Day 2020 |
В некоторых задачах в пользовательских модулях возможно запретить использовать привязки в библиотекам и запретить использовать SYSTEM. И в таком виде уже безопаснее применять модули расширений, распространяемые в открытых исходных кодах. |
Автор: | Дмитрий Дагаев [ Вторник, 02 Февраль, 2021 16:20 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Да, правильно, запретить SYSTEM, запретить POINTER. |
Автор: | Comdiv [ Вторник, 02 Февраль, 2021 16:24 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Этого всё равно недостаточно |
Автор: | Иван Денисов [ Вторник, 02 Февраль, 2021 16:48 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Comdiv писал(а): Этого всё равно недостаточно А как тогда можно на ББ что-то выполнить системное? За массивы не вылезешь ведь. Если честно, то вопрос актуален, хотелось бы иметь возможность придумать систему безопасных ограничений, чтобы не обойти было. |
Автор: | Дмитрий Дагаев [ Вторник, 02 Февраль, 2021 17:13 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Comdiv писал(а): Этого всё равно недостаточно Неправильно поставлен вопрос. Нужно начинать с "микро-мира". 1. Вот FPGA - можно ли тут запретить динамическую память? Можно, особенно, если ее там нет. 2. Вот ПО для контроллеров, O7. Уже есть динамическая память, но запретить можно. 3. Вот A2 - тут уже функциональности побольше. И закрывать побольше. 4. Ну и наконец, BlackBox запущенный поверх Win/Lin - ОС, где дырка на дырке сидит и дыркой погоняет. Тут надо много чего закрывать. И все равно останутся лазейки. А другого-то выхода и нет... |
Автор: | Trurl [ Вторник, 02 Февраль, 2021 17:33 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Comdiv писал(а): Но я и говорю, что в алгоритмически полном языке нельзя ничего запретить статически на уровне компиляции. Но ведь алгоритмически полные языки существуют только в учебниках по матлогике. |
Автор: | Comdiv [ Вторник, 02 Февраль, 2021 18:07 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Дмитрий Дагаев писал(а): 1. Вот FPGA - можно ли тут запретить динамическую память? Можно, особенно, если ее там нет. Нельзя даже если её там нет, тем более, что и в любом компьютере нет динамической памяти - всё статично. Остальное - это игры в имитацию, которые можно производить в самых разных терминах на самых разных уровнях. Например, в этой программе на Обероне есть и динамическое выделение и операции с 32-битными беззнаковыми числами, но нет ни NEW и POINTER, ни UNSIGNED, ни SYSTEM.
|
Автор: | Comdiv [ Вторник, 02 Февраль, 2021 18:09 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Trurl писал(а): Comdiv писал(а): Но я и говорю, что в алгоритмически полном языке нельзя ничего запретить статически на уровне компиляции. Но ведь алгоритмически полные языки существуют только в учебниках по матлогике. |
Автор: | Дмитрий Дагаев [ Вторник, 02 Февраль, 2021 18:12 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Я имитациями не занимаюсь. Форумная перманентная борьба также не интересна. Если есть вопрос - отвечу. |
Автор: | Comdiv [ Вторник, 02 Февраль, 2021 18:13 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Иван Денисов писал(а): Comdiv писал(а): Этого всё равно недостаточно А как тогда можно на ББ что-то выполнить системное? За массивы не вылезешь ведь. Если честно, то вопрос актуален, хотелось бы иметь возможность придумать систему безопасных ограничений, чтобы не обойти было. |
Автор: | Comdiv [ Вторник, 02 Февраль, 2021 18:15 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Дмитрий Дагаев писал(а): Я имитациями не занимаюсь. Форумная перманентная борьба также не интересна. Если есть вопрос - отвечу. Это не о форумной борьбе, а алгоритмической полноте и её свойствам, не более. Игра в имитацию - это такой термин, может, и не особо удачный, но, например, теория игр тоже не о тех играх, о которых можно подумать.
|
Автор: | adimetrius [ Вторник, 02 Февраль, 2021 18:42 ] |
Заголовок сообщения: | Re: OS Day 2020 |
А какие могут возникнуть ошибки, если программа размещает, например, динамические данные в статических массивах? (Если я правильно понял, вы это назвали имитацией.) |
Автор: | Comdiv [ Вторник, 02 Февраль, 2021 18:45 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Всё те же - нехватка памяти, в том числе из-за утечек, её порча, длительность и плохая предсказуемость времени на выделение и освобождение. |
Автор: | Sergej Durmanov [ Вторник, 02 Февраль, 2021 19:02 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Comdiv писал(а): Этого всё равно недостаточно Недостаточно для чего? Область распространения гарантий не должна превышать область определения. Языковые гарантии распространяются на язык. Не языковые гарантии и решаются не языковыпи средствами - например, средствами разграничения доступа. В Активном Обероне, в процедурах и активностях, помеченных как realtime, запрещено использовать операцию NEW. Но и напрямую, например Heaps.NewRec, Heaps.NewArr тоже не вызвать - потому что из кода реального времени можно обратиться только к сущностям реального времени. Это языковые гарантии, которые обеспечивает компилятор. Конечно, можно извратиться и эти гарантии обойти низкоуровневыми средствами, которые в общем и призваны нарущать гарантии - но это уже выходит за область определения языковых гарантий и должно решаться другими средствами. Поэтому, применительно к запрету выделения памяти в соответствующих участках кода, языковые гарантии ( воплощенные в компиляторе ) более чем достаточны. |
Автор: | Comdiv [ Вторник, 02 Февраль, 2021 19:37 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Недостаточно для доказательства заявленных свойств программы. Недостаточно и при отсутствии обращения к низкоуровневым средствам. Но мы уже выяснили, что с Иваном говорим о разном. |
Автор: | PSV100 [ Пятница, 12 Февраль, 2021 17:33 ] |
Заголовок сообщения: | Re: OS Day 2020 |
На сегодня разработчики Ada/SPARK также озадачены возникшими здесь вопросами, но проблематика представляется с иной стороны. Среди их пользователей есть неудовлетворенность в действующих ограничениях "вычислительных возможностей" (ограничения использования Heap, указателей и пр., принуждающие выстраивать динамические структуры на базе статических массивов и т.д.) и возникающих в результате трудностях верификации. Для следующего стандарта Ada/SPARK (который, вроде бы, уже доступен) внедрено расширение -- вводятся ограниченные указатели и динамическое управление памятью: * введение: Safe Dynamic Memory Management in Ada and SPARK * документация: https://docs.adacore.com/spark2014-docs/html/lrm/declarations-and-types.html#access-types * подробно: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0240-1.txt Для указателей (access types в Ada) вводится семантика "владеющих" указателей, с передачей прав владения объектом (временное или нет), с возможностью совместного доступа на чтение. Распределение памяти автоматическое без сборщика мусора (и без reference counting и т.п.). Подробные описания объёмные, в целом семантика интуитивно понятна (см. введение выше). Отчасти напоминает технику "borrow checker" в Rust (его опыт также учитывался), но в Ada модель выглядит попроще. Ключевое: семантика таких указателей применима для верификации, причём с учётом "фишки" SPARK -- запрета алиасов (возникновение множества ссылок на изменяемый в данной области объект кроме специализированных "конкурентных" объектов при многопоточном доступе). Я не в курсе, как нововведения уживаются со стандартами безопасности (вроде бы, тамошний silver level и выше (в SPARK несколько уровней верификации) отвечают требованиям различных отраслевых стандартов и дают возможность для сертификации, вместе с указателями, получается что ли...). Также я не в курсе насчёт принципов низкоуровневого устройства менеджера памяти. Я не знаток Ada, но, вроде бы, в основном стандартные аллокаторы работают на принципах пулов объектов по типам. Видимо, вопросы дефрагментации памяти, предаллокации и пр. как-то решаются (там тьма всяких "аспектов" и "прагм"). Например, в Safety-Critical Java Specification имеется даже специализированное API для некоторого управления аллокатором (там также есть возможность для автоматической памяти без сборщика мусора, на основе регионов, но гораздо муторнее, чем предлагается в Ada, без контроля алиасов и пр.). В общем, в некотором смысле проблемы косвенного доступа, о котором речь была выше в топике, в Ada/SPARK пытаются решить в том числе с помощью расширения возможностей прямого доступа (его "выпрямления", предполагающего уменьшение усилий для доказательств согласно заявлениям разработчиков). |
Автор: | PSV100 [ Пятница, 12 Февраль, 2021 17:36 ] |
Заголовок сообщения: | Re: OS Day 2020 |
Следует отметить, что указатели выше это именно "владеющие" указатели с ограниченной семантикой, они не могут быть "косвенными" без права владения ака простая ссылка. Так, с их помощью можно задать, например, рекурсивные (расширяемые/уменьшаемые) структуры аля однонаправленный список, но нельзя задать "просто" ссылку в структуре (поле объекта) на "предыдущую" запись в двунаправленном списке или в целом иметь "произвольный" указатель (временные "владеющие" указатели возможны в качестве локальных переменных и параметров процедур с автоматическим разруливанием прав владения). Для циклических структур или условного графа, или в целом для произвольного доступа по-прежнему предлагается сводить алгоритмику к массивам и операции индексации. Ранее предполагался и иной вариант указателей -- так называемые Fenced-указатели как ограниченные в контексте некоторого типа (региона как пула объектов) двух видов -- владеющего объектом или нет: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0240-2.txt Пример определения типа как двунаправленный список, где Node_Ptr -- тип-указатель на Node, для которого задан "аспект" Fenced ассоциированный с типом List (привязали к пулу объектов), для полей-указателей определены "аспекты" Owner или Unmanaged (владеющий или нет): Код: type Node; type Node_Ptr is access Node with Fenced => (List); type Node is limited record Elem : Element_Type; Prev : Node_Ptr with Unmanaged; Next : Node_Ptr with Owner; end record; type List is ... with record Head : Node_Ptr with Owner; ... end record; Вариант указателей выше ака "сильная" и "слабая" ссылка, вроде бы, не взлетел. Сейчас привязку к регионам осуществляют автоматически. Слабые (произвольные) ссылки, как я понимаю, пока очень проблемны для верификации в SPARK и вводить их не собираются в ближайшие времена. |
Автор: | PSV100 [ Пятница, 12 Февраль, 2021 17:43 ] |
Заголовок сообщения: | Re: OS Day 2020 |
У AdaCore есть ещё один любопытный вариант "указателей с гарантией". К слову, тренировки с указателями для SPARK там были ещё до появления Rust в массы -- в рамках экспериментального языка ParaSail (Parallel Specification and Implementation Language): https://adacore.github.io/ParaSail/ Это Ada-подобный язык с гарантиями в стиле высоких уровней SPARK (без exception, без runtime-проверок (ака выход за границы массива, переполнения и т.п.) -- статические доказательства). Владеющих указателей в языке нет, но они замаскированы в виде опциональных типов -- любой тип может быть объявлен с модификатором optional, и его значение тогда может принимать в том числе и null (как в SQL, например). Для облегчения работы с такими типами кроме копирования введены стандартные операции перемещения (move как оператор "<==") и обмена (swap: "<=>"). В SPARK семантика опциональных типов переехала на обычные указатели с привычной операцией копирования (которая иногда работает как перемещение, при необходимости источник для копирования может быть установлен в null). А также в язык введены временные ссылки как переменные, объявляемые через "ref" вместо "var". Пример: Код: func Expand (var HT : Hash_Table) is // Double the size of the Hash_Table backbone var Old_Backbone <== HT.Backbone // Move old backbone to temp const New_Len := |Old_Backbone| * 2 // Create backbone with double the number of buckets HT.Backbone := Create(New_Len, null) for each Old_Bucket of Old_Backbone loop for Old_Elem => Old_Bucket then Old_Elem.Next while Old_Elem not null loop const New_Hash := Hash(Key_Of(Old_Elem.Entry)) mod New_Len ref New_Bucket => HT.Backbone[New_Hash + 1] // Insert at front, using ``move''s to create new node. New_Bucket := Node::(Entry <== Old_Elem.Entry, Next <== New_Bucket) end loop end loop end func Expand Выше переменная "ref New_Bucket", инициализируемая через "=>", является ака временным (не владеющим) указателем, принимающим такие же права (чтение/запись) как у исходного объекта (и разделяет с ним доступ с контролем уникальности прав на изменение). Аргументы для for-циклов также являются ссылками. Ссылки могут быть только как локальные объекты, они не являются частью так называемого "object declaration" -- не могут быть в составе записей (структур). Параметры процедур также могут быть ссылками, в том числе и в качестве возвращаемых, но только на объект, содержащийся в аргументах процедуры в виде ссылки, или его часть. Например, через ссылки работают операции индексации, которые можно определить для своих типов: Код: interface PSL::Containers::Hash_Table<KV_Type is Keyed<>> is ... // объявление оператора "[...]", с предусловием op "indexing"(ref T: Hash_Table; Key: KV_Type::Key_Type){Key in T} -> ref KV_Type ... end interface PSL::Containers::Hash_Table В общем, у AdaCore есть наработки для временных ссылок (дающих некоторое удобство и скорость/экономию ресурсов) и унификации произвольного доступа (обобщённая подконтрольная индексация). С учётом того, что фишки ParaSail сейчас перелазят в новый стандарт Ada (методики параллельного программирования, вариации циклов, в том числе параллельных, те же владеющие указатели и пр.), можно предположить, что и ссылки с индексацией каким-то образом подтянутся в Ada/SPARK. Очень достойный симбиоз вырисовывается... |
Автор: | Дмитрий Дагаев [ Воскресенье, 03 Июль, 2022 17:21 ] | ||
Заголовок сообщения: | Re: OS Day 2020 | ||
Завершилась IX международная научно-практическая конференция OS DAY 2022 – технологическое обеспечение безопасности операционных систем. Я принял участие с докладом "Архитектурные принципы построения программной платформы АСУ ТП АЭС для обеспечения живучести", аннотация здесь. Мой доклад это первый день, начинается с https://youtu.be/nJEff3tKL8o?t=25085
|
Страница 2 из 2 | Часовой пояс: UTC + 3 часа |
Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |