Блог

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 и 95http://en.wikipedia.org/wiki/SPARK_(programming_language). Я предполагаю, что у SPARK нет версии для более поздних версий Ada, потому что еще слишком рано говорить о том, насколько безопасны новые версии на самом деле. В последней статье также упоминается, что Ada может быть оптимизирован для скоростей, конкурирующих с C, что было бы важно для приложений реального времени, которые полагаются на точный контроль во время быстро меняющихся событий. Существует множество встроенных стандартных функций для управления в режиме реального времени, которые, очевидно, важны для языка, критичного для безопасности.