Подтвердить что ты не робот

Как Ада является "критическим для безопасности" языком?

Я пробовал поиск в Интернете и читал некоторые фрагменты в Интернете. Почему Ада является "критическим для безопасности" языком? Некоторые вещи, которые я замечаю,

  • Нет указателей
  • Укажите диапазон (этот тип является целым числом, но может быть только 1-12)
  • Явно указать, если параметр функции отсутствует или находится в/из
  • Циклы на основе диапазона (во избежание ошибок привязки или проверки привязки)

Остальная часть синтаксиса я либо не понимал, либо не видел, как это помогает ему быть "критически важным". Это некоторые моменты, но я не вижу большой картины. Есть ли у меня дизайн по контракту, которого я не вижу? Имеет ли он правила, которые усложняют компиляцию кода (и если да, то какие?) Почему это "критически важный для безопасности" язык?

4b9b3361

Ответ 1

Все это полезно для критически важных приложений; но рассмотрите также возможность назначить макет (вплоть до битов) и возможность [опционально] указать, что такая запись может ТОЛЬКО находиться в определенном месте (полезно для таких вещей, как сопоставления видеопамяти).

Считайте, что многие критически важные для безопасности приложения также не имеют стандартного (в смысле как "широко распространенного", так и прямого сравнения) интерфейсов; Например: ядерные реакторы, ракетные двигатели (сама техника отличается от поколения к поколению *), модели самолетов.

Предстоящий стандарт Ada 2012 имеет фактические контракты в форме до- и пост-условий; Пример (взято из http://www2.adacore.com/wp-content/uploads/2006/03/Ada2012_Rational_Introducion.pdf):

generic
   type Item is private;
package Stacks is

type Stack is private;

function Is_Empty(S: Stack) return Boolean;
function Is_Full(S: Stack) return Boolean;

procedure Push(S: in out Stack; X: in Item)
with
    Pre => not Is_Full(S),
    Post => not Is_Empty(S);

procedure Pop(S: in out Stack; X: out Item)
with
    Pre => not Is_Empty(S),
    Post => not Is_Full(S);

Stack_Error: exception;

private
 -- Private portion.
end Stacks;

Кроме того, еще одна вещь, которая затушевывается, - это возможность исключить Null из ваших типов Access/pointer; это полезно в том, что вы можете: a) указать это исключение в ваших параметрах подпрограммы и b) упорядочить ваш алгоритм [поскольку вам не нужно проверять значение null на каждом экземпляре использования] и c) разрешить исключение обработчик обрабатывает (я предполагаю) исключительное обстоятельство a Null.

* The Arianne 5 disaster occurred precisely because the management disregarded this fact and had the programmers use the incorrect specifications: that of the Arianne 4.

Ответ 2

Хорошо, это довольно просто. Причина в том, что много Ada sytax, похоже, не имеет ничего общего с тем, чтобы сделать язык "критичным для безопасности" (что бы это ни значило для языка) заключается в том, что это не цель дизайна Ada. Он был разработан как скомпилированный системный язык программирования общего назначения, достаточно способный, чтобы министерство обороны США могло избавиться от всех своих маленьких одноразовых языков, которые оно должно было поддерживать повсюду.

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

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

Ответ 3

AdaCore имеет приятную презентацию различных функций безопасности Ada 2005 здесь:

http://www.adacore.com/knowledge/technical-papers/safe-secure/

Правительство и промышленность США также давно изучали надежность программ, сравнивая языки. Я не мог найти его очень быстро, поскольку сайты все старые (!), Но здесь цитата из сайта DDCI: "В исследованиях, проведенных в 80-х годах, Ada последовательно превзошла установленные языки программирования, такие как Pascal, Fortran и C. В девяностые годы, Ada продолжает превзойти С++ в оценке производительности, измеряя возможности, эффективность, обслуживание, риск и стоимость жизненного цикла."

Перечислите причины, по которым они использовали его в проекте Commanche, в ссылке ниже. Я добавлю, что реализации платформы были в течение долгого времени и остались стабильными. Как и источник в статье, техническое обслуживание - это то место, где приходит большинство затрат. Мы видели, что современные соперники .NET и Java меняются как сумасшедшие. Долгосрочная стабильность Ada лучше для важных для безопасности приложений, которые часто выставляются на длительные периоды (иногда десятилетия).

http://www.ddci.com/displayNews.php?fn=programs_rah66.php

Другим преимуществом является то, что Ada была разработана для кросс-языкового развития. Я постоянно вижу в новостях, что люди говорят о том, как .NET и JVM являются инновационными b/c, которые позволяют вам смешивать "правильные инструменты для работы" в одной системе. У Ады была эта способность в течение длительного времени. Обычно приложения являются сочетанием Ada, C, С++, ассемблера и т.д. (MULTOS CA приходит на ум.) И они все еще хорошо функционируют.

Он также не был статическим. Они продолжают обновлять язык, совсем недавно в 2012 году. Его портативность позволила ему работать как на JVM, так и на .NET тоже для людей, которым нужны библиотеки или есть много существующего кода на них. Существуют также инструменты разработки Ada и надежные среды выполнения для многих ОС и RTOS от IBM, Aonix, AdaCore и Green Hills.

Последнее преимущество: если оно будет скомпилировано, оно будет работать. Как правило.

Ответ 4

Ada имеет превосходную поддержку в режиме реального времени http://www.adaic.org/resources/add_content/standards/05rat/html/Rat-1-3-4.html. Это позволяет программисту реализовать большую степень детерминизма, а не беспокоиться о технических деталях самого языка программирования. Хотя многие функции времени исполнения, поддерживаемые Ada, могут быть достигнуты на C с некоторым глубоким пониманием вещей, Ada обеспечивает большинство функций реального времени очень хорошо, так как она стандартизирована. У Ada даже есть профиль Ravenscar http://en.wikipedia.org/wiki/Ravenscar_profile и SPARK - компьютерный язык, на котором важна "высоконадежная операция", основанная на подмножестве Ada 83 и 95 http://en.wikipedia.org/wiki/SPARK_%28programming_language%29. Я предполагаю, что у SPARK нет версии для более поздних версий ada b/c, пока еще рано говорить о том, насколько безопасны новые версии. В последней статье также упоминается, что Ada может быть оптимизирована для скоростей, конкурирующих с C, что было бы важно для приложений реального времени, которые полагались на точный контроль во время быстро меняющихся событий. Есть много встроенных стандартных функций для управления в реальном времени, которые, очевидно, важны для "критически важного" языка.