OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Воскресенье, 18 Апрель, 2021 02:23

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




Начать новую тему Ответить на тему  [ Сообщений: 38 ]  На страницу Пред.  1, 2
Автор Сообщение
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 16:14 
Аватара пользователя

Зарегистрирован: Четверг, 08 Октябрь, 2009 15:00
Сообщения: 3056
В некоторых задачах в пользовательских модулях возможно запретить использовать привязки в библиотекам и запретить использовать SYSTEM. И в таком виде уже безопаснее применять модули расширений, распространяемые в открытых исходных кодах.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 16:20 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 554
Откуда: Москва
Да, правильно, запретить SYSTEM, запретить POINTER.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 16:24 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1283
Откуда: Киев
Этого всё равно недостаточно


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 16:48 
Аватара пользователя

Зарегистрирован: Четверг, 08 Октябрь, 2009 15:00
Сообщения: 3056
Comdiv писал(а):
Этого всё равно недостаточно

А как тогда можно на ББ что-то выполнить системное? За массивы не вылезешь ведь. Если честно, то вопрос актуален, хотелось бы иметь возможность придумать систему безопасных ограничений, чтобы не обойти было.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 17:13 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 554
Откуда: Москва
Comdiv писал(а):
Этого всё равно недостаточно

Неправильно поставлен вопрос.

Нужно начинать с "микро-мира".
1. Вот FPGA - можно ли тут запретить динамическую память? Можно, особенно, если ее там нет.
2. Вот ПО для контроллеров, O7. Уже есть динамическая память, но запретить можно.
3. Вот A2 - тут уже функциональности побольше. И закрывать побольше.
4. Ну и наконец, BlackBox запущенный поверх Win/Lin - ОС, где дырка на дырке сидит и дыркой погоняет. Тут надо много чего закрывать. И все равно останутся лазейки.

А другого-то выхода и нет...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 17:33 

Зарегистрирован: Понедельник, 28 Ноябрь, 2005 10:28
Сообщения: 1366
Comdiv писал(а):
Но я и говорю, что в алгоритмически полном языке нельзя ничего запретить статически на уровне компиляции.

Но ведь алгоритмически полные языки существуют только в учебниках по матлогике. :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 18:07 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1283
Откуда: Киев
Дмитрий Дагаев писал(а):
1. Вот FPGA - можно ли тут запретить динамическую память? Можно, особенно, если ее там нет.
Нельзя даже если её там нет, тем более, что и в любом компьютере нет динамической памяти - всё статично. Остальное - это игры в имитацию, которые можно производить в самых разных терминах на самых разных уровнях. Например, в этой программе на Обероне есть и динамическое выделение и операции с 32-битными беззнаковыми числами, но нет ни NEW и POINTER, ни UNSIGNED, ни SYSTEM.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 18:09 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1283
Откуда: Киев
Trurl писал(а):
Comdiv писал(а):
Но я и говорю, что в алгоритмически полном языке нельзя ничего запретить статически на уровне компиляции.
Но ведь алгоритмически полные языки существуют только в учебниках по матлогике. :)
Всего лишь нет смысла постоянно повторять "за исключением бесконечной памяти". Поэтому существуют, а эту оговорку держите в уме.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 18:12 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 554
Откуда: Москва
Я имитациями не занимаюсь. Форумная перманентная борьба также не интересна. Если есть вопрос - отвечу.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 18:13 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1283
Откуда: Киев
Иван Денисов писал(а):
Comdiv писал(а):
Этого всё равно недостаточно

А как тогда можно на ББ что-то выполнить системное? За массивы не вылезешь ведь. Если честно, то вопрос актуален, хотелось бы иметь возможность придумать систему безопасных ограничений, чтобы не обойти было.
Мы немного о разном. Чтобы не обойти было - так это вообще фантастика, но чтобы уменьшить риск - изоляцию надо проводить с более сильными ограничениями не только для прямого доступа, но и косвенного.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 18:15 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1283
Откуда: Киев
Дмитрий Дагаев писал(а):
Я имитациями не занимаюсь. Форумная перманентная борьба также не интересна. Если есть вопрос - отвечу.
Это не о форумной борьбе, а алгоритмической полноте и её свойствам, не более. Игра в имитацию - это такой термин, может, и не особо удачный, но, например, теория игр тоже не о тех играх, о которых можно подумать.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 18:42 
Аватара пользователя

Зарегистрирован: Суббота, 16 Февраль, 2008 02:47
Сообщения: 459
А какие могут возникнуть ошибки, если программа размещает, например, динамические данные в статических массивах? (Если я правильно понял, вы это назвали имитацией.)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 18:45 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1283
Откуда: Киев
Всё те же - нехватка памяти, в том числе из-за утечек, её порча, длительность и плохая предсказуемость времени на выделение и освобождение.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 19:02 

Зарегистрирован: Пятница, 11 Январь, 2019 19:26
Сообщения: 216
Откуда: Russia
Comdiv писал(а):
Этого всё равно недостаточно

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

В Активном Обероне, в процедурах и активностях, помеченных как realtime, запрещено использовать операцию NEW. Но и напрямую, например Heaps.NewRec, Heaps.NewArr тоже не вызвать - потому что из кода реального времени можно обратиться только к сущностям реального времени. Это языковые гарантии, которые обеспечивает компилятор.
Конечно, можно извратиться и эти гарантии обойти низкоуровневыми средствами, которые в общем и призваны нарущать гарантии - но это уже выходит за область определения языковых гарантий и должно решаться другими средствами. Поэтому, применительно к запрету выделения памяти в соответствующих участках кода, языковые гарантии ( воплощенные в компиляторе ) более чем достаточны.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Вторник, 02 Февраль, 2021 19:37 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1283
Откуда: Киев
Недостаточно для доказательства заявленных свойств программы. Недостаточно и при отсутствии обращения к низкоуровневым средствам.
Но мы уже выяснили, что с Иваном говорим о разном.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Пятница, 12 Февраль, 2021 17:33 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 442
На сегодня разработчики 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 пытаются решить в том числе с помощью расширения возможностей прямого доступа (его "выпрямления", предполагающего уменьшение усилий для доказательств согласно заявлениям разработчиков).


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Пятница, 12 Февраль, 2021 17:36 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 442
Следует отметить, что указатели выше это именно "владеющие" указатели с ограниченной семантикой, они не могут быть "косвенными" без права владения ака простая ссылка. Так, с их помощью можно задать, например, рекурсивные (расширяемые/уменьшаемые) структуры аля однонаправленный список, но нельзя задать "просто" ссылку в структуре (поле объекта) на "предыдущую" запись в двунаправленном списке или в целом иметь "произвольный" указатель (временные "владеющие" указатели возможны в качестве локальных переменных и параметров процедур с автоматическим разруливанием прав владения). Для циклических структур или условного графа, или в целом для произвольного доступа по-прежнему предлагается сводить алгоритмику к массивам и операции индексации.

Ранее предполагался и иной вариант указателей -- так называемые 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 и вводить их не собираются в ближайшие времена.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: OS Day 2020
СообщениеДобавлено: Пятница, 12 Февраль, 2021 17:43 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 442
У 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. Очень достойный симбиоз вырисовывается...


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 38 ]  На страницу Пред.  1, 2

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


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

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


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

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