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

Question

Я попробовал поискать в Интернете и прочитать некоторые фрагменты в Интернете.Почему Ada является «критичным по отношению к безопасности» языком?Некоторые вещи, которые я замечаю:

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

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

Answer 1

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

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

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

Answer 2

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

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

У будущего стандарта 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 / типов указателей; это полезно в том, что вы можете) указать это исключение в параметрах вашей подпрограммы, и б) упростить ваш алгоритм [поскольку вам не нужно проверять нулевое значение в каждом случае использования], и в) позволить обработчику исключений обрабатывать (я полагаю) исключительныйобстоятельства 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.

Answer 3

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

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

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

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

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

Еще одно преимущество - Ada была разработана для межъязыковой разработки.Я постоянно вижу в новостях людей, говорящих о том, что .NET и JVM являются инновационными, потому что они позволяют вам смешивать «правильные инструменты для работы» в одной системе.Ада обладала такой способностью в течение длительного времени.Обычно приложения представляют собой смесь Ada, C, C ++, ассемблера и т. Д. (MULTOS CA приходит на ум). И они все еще работают хорошо.

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

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

Answer 4

Я знаю, что уже поздно, но это пример, с которым я недавно столкнулся. Я написал следующую функцию C ++, которая прекрасно работала в -O0:

size_t get_index(const Monomial & t, const Monomial & u) {
    get_index(t, u.log()); // forgot to type "return" first...
}

Это на самом деле компилируется, и хотя оно может выдать предупреждение, если вам повезет с приличным компилятором, вы вряд ли увидите его, когда одна из многих программ компилируется. Чудесно, он работал нормально, когда я скомпилировал его с -O0. Но когда я скомпилировал его в -O3, он каждый раз падал, и я не мог понять почему, потому что не видел предупреждения (если оно вообще появилось). Представьте себе отладку, когда вы думаете, что представляете return просто потому, что знаете свое намерение.

Точно так же, когда я изучал C, я часто совершал эту ошибку:

int a;
scanf("%d", a); /* left out & before the a */

Использование int для указателей и наоборот считается нормальной практикой программирования на C, настолько, что компиляторы 25 лет назад даже не удосужились выдать предупреждение. Черт, это была функция C, а не ошибка . (См., Например, Брайан Кернаган «Почему Паскаль не мой любимый язык».) И, конечно, тогда домашние компьютерные ОС не имели защиты памяти; если вам повезло, компьютер не записывал данные на жесткий диск при перезагрузке.

Такого рода ошибки не будут даже компилироваться в Аде. Функции имеют для возврата значения, и вы не можете случайно использовать Integer вместо access Integer (т.е. указатель на целое число).

И это только начало!

Answer 5

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