Исследование корректности реализации и верификация АС

Понятие корректности или правильности подразумевает соответст­вие проверяемого объекта некоторому эталонному обьекту или совокуп­ности формализованных эталонных характеристик и правил. Корректность ПО при разработке наиболее полно определяется степенью соответствия предъявляемым к ней формализованным требованиям программной спе­цификации. В спецификациях отражается совокупность эталонных харак­теристик, свойств и условий, которым должна соответствовать программа. Основную часть спецификации составляют функциональные критерии и характеристики. Исходной программной спецификацией, которой должна соответствовать программа, является ТЗ.

При отсутствии полностью формализованной спецификации требо­ваний в качестве ТЗ, которому должна соответствовать АС и результаты ее функционирования, иногда используются неформализованные пред­ставления разработчика, пользователя или заказчика программ. Однако понятие корректности программ по отношению к запросам пользователя или заказчика сопряжено с неопределённостью самого эталона, которому должна соответствовать АС. Для сложных программ всегда существует риск обнаружить их некорректность (по мнению пользователя или заказ­чика) при формальной корректности относительно спецификаций вслед­ствие неточности самих спецификаций.

Традиционный взгляд на спецификацию требований заключается в том, что она представляет собой документ на естественном языке, кото­рый является интерфейсом между заказчиком и изготовителем. Хотя под­готовке документа может предшествовать некоторое взаимодействие, именно этот документ в значительной степени выступает как "отправная точка" для изготовителя программ.

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

• быть формальными;

• позволять проверять непротиворечивость и полноту требований заказ­чика;

• служить основой для дальнейшего формализованного проектирования ОС.

Существует несколько подходов к определению спецификаций тре­бований.

Спецификация как описание. Заказчик выдает спецификацию, чтобы изготовители могли снабдить его тем изделием, которое он желает, по­этому заказчик видит этот документ главным образом как описание сис­темы, которую он желал бы иметь. В принципе, в описании должно быть указано, что должна и что не должна делать система. На практике обычно по умолчанию предполагается, что система должна делать то, что уточ­няется в спецификации, и не должна делать ничего более. В этом состоит главная проблема с описательной стороной спецификации. Предполага­ется, что заказчик всегда точно знает всё, что система должна и не долж­на делать. Более того, в дальнейшем предполагается, что заказчик пол­ностью перенёс это знание в специфицированный документ.

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

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

Спецификация как модель. Современные более строгие представле­ния о спецификации трактуют ее как модель системы. При условии, что лежащая в основе модели семантика в достаточной мере обоснована, такая спецификация обеспечивает чёткую формулировку требований.

Соответствующие модели подходят также для автоматизированного контроля целостности и другого прогнозного анализа, который, в частно­сти, обеспечит прекращение разработки системы, в принципе не способ­ной удовлетворить требованиям.

Модели как описание системы имеют следующие отличительные черты по сравнению сдругими способами формального описания:

• хорошее сочетание нисходящего и восходящего подходов к их разра­ботке с возможностью выбора абстрактного описания;

• возможность описания параллельной, распределенной и циклической работы;

• возможность выбора различных формализованных аппаратов для описания систем.

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

Так как целевым объектом проектирования является АС, то модель может описывать либо саму АС, либо ее поведение, т.е. внешние прояв­ления функционирования АС. Модель, описывающая поведение АС по сравнению с моделью АС, обладает одним важным преимуществом - она может быть проверена и оценена как исполнителями, так и заказчиками, поскольку заказчики не знают, как должна работать АС, но зато они пред­ставляют, что она должна делать. В результате такого моделирования может быть проверена корректность спецификаций относительно исход­ной постановки задачи, т.е. ТЗ. Кроме того, критерии правильности счи­таются достаточными при условии, что спецификация представляет собой исчерпывающее описание "внешнего" поведения объекта при всех воз­можных (или запланированных) ситуациях его использования.

Как было отмечено выше, при разработке АС, особенно ее компо­нентов, представляющих систему защиты информации, для обеспечения высоких гарантий отсутствия неисправностей и последующего доказа­тельства того, что система функционирует согласно требованиям ТЗ, ис­пользуются формальные подходы к ее проектированию.

Формальное проектирование алгоритмов базируется, в основном, на языках алгоритмических логик, которые включают высказывание вида

Q {S} R,

читающееся следующим образом: "если до исполнения оператора S было выполнено условие Q, то после него будет R". Здесь Q называется преду­словием, a R - постусловием. Эти языки были изобретены практически одновременно Р.У.Флойдом (1967г.), С.А.Р.Хоаром (1969г.) и учеными польской логической школы (А. Сапьвицкий и др., 1970 г.}. Как предусло­вие, так и постусловие являются предикатами.

Рассмотрение программ в качестве некоего "преобразователя пре­дикатов" позволяет прямо определить связь между начальными и конеч­ными состояниями без каких-либо ссылок на промежуточные состояния, которые могут возникнуть во время выполнения программы.

Преимущество представления алгоритма в виде преобразователя предикатов состоит в том, что оно дает возможность:

• анализировать алгоритмы как математические обьекты;

• дать формальное описание алгоритма, позволяющее интеллектуально охватить алгоритм;

• синтезировать алгоритмы по представленным спецификациям;

• провести формальное верифицирование алгоритма, т.е. доказать кор­ректность его реализации.

Методология формальной разработки и доказательства корректности алгоритмов в настоящее время хорошо разработана и изложена в целом ряде работ. Вкратце суть этих методов сводится к следующему:

• разработка алгоритма проводится методом последовательной деком­позиции, с разбивкой общей задачи, решаемой алгоритмом, на ряд более мелких подзадач;

• критерием детализации подзадач является возможность их реализа­ции с помощью одной конструкции ветвления или цикла;

• разбиение общей задачи на подзадачи предусматривает формулиро­вание пред- и постусловий для каждой подзадачи с целью их коррект­ного проектирования и дальнейшей верификации.

Для доказательства корректности алгоритма (верификация) форму­лируется математическая теорема Q{S}R, которая затем доказывается. Доказательство теоремы о корректности принято разбивать на две части. Одна часть служит для доказательства того, что рассматриваемый алго­ритм вообще может завершить работу (проводится анализ всех циклов). В другой части доказывается корректность постусловия в предположении, что алгоритм завершает работу.

 

Теория безопасных систем (ТСВ)

Понятие "доверенная вычислительная среда" (trusted computing base - TCB) появилось в зарубежной практике обеспечения информаци­онной безопасности достаточно давно. Смысл характеристики "дове­ренная" можно пояснить следующим образом.

Дискретная природа характеристики "безопасный" (в том смысле, что либо нечто является безопасным, полностью удовлетворяя ряду предъ­являемых требований, либо не является, если одно или несколько требо­ваний не выполнены) в сочетании с утверждением "ничто не бывает безо­пасным на сто процентов" подталкивают к тому, чтобы вести более гибкий термин, позволяющий оценивать то, в какой степени разработанная за­щищенная АС соответствует ожиданиям заказчиков. В этом отношении характеристика "доверенный" более адекватно отражает ситуацию, где оценка, выраженная этой характеристикой (безопасный или доверенный), основана не на мнении разработчиков, а на совокупности факторов, вклю­чая мнение независимой экспертизы, опыт предыдущего сотрудничества с разработчиками, и в конечном итоге, является прерогативой заказчика, а не разработчика.

Доверенная вычислительная среда (ТСВ) включает все компоненты и механизмы защищенной автоматизированной системы, отвечающие за реализацию политики безопасности (понятие политики безопасности рас­сматривается в гл. 4). Все остальные части АС, а также ее заказчик пола­гаются на то, что ТСВ корректно реализует заданную политику безопасно­сти даже в том случае, если отдельные модули или подсистемы АС раз­работаны высококвалифицированными злоумышленниками с тем, чтобы вмешаться в функционирование ТСВ и нарушить поддерживаемую ею политику безопасности.

Минимальный набор компонентов, составляющий доверенную вы­числительную среду, обеспечивает следующие функциональные возмож­ности:

• взаимодействие с аппаратным обеспечением АС;

• защиту памяти;

• функции файлового ввода-вывода;

• управление процессами.

Некоторые из перечисленных компонентов были рассмотрены в дан­ном разделе.

Дополнение и модернизация существующих компонентов АС с уче­том требований безопасности могут привести к усложнению процессов сопровождения и документирования. С другой стороны, реализация всех перечисленных функциональных возможностей в рамках централизован­ной доверенной вычислительной среды в полном объеме может вызвать разрастание размеров ТСВ и, как следствие, усложнение доказательства корректности реализации политики безопасности. Так, операции с файла­ми могут быть реализованы в ТСВ в некотором ограниченном объеме, достаточном для поддержания политики безопасности, а расширенный ввод-вывод в таком случае реализуется в той части АС,,которая находит­ся за пределами ТСВ. Кроме того, необходимость внедрения связанных с безопасностью функций во многие компоненты АС, реализуемые в раз­личных модулях АС, приводит к тому, что защитные функции распреде­ляются по всей АС, вызывая аналогичную проблему.

Представляется оправданной реализация доверенной вычислитель­ной среды в виде небольшого и эффективного (в терминах исполняемого кода} ядра безопасности (см. гл.4), где сосредоточены все механизмы обеспечения безопасности. В связи с перечисленными выше соображе­ниями, а также с учетом определенной аналогии между данными поня­тиями такой подход предполагает изначальное проектирование АС с уче­том требований безопасности. При этом в рамках излагаемой теории оп­ределены следующие этапы разработки защищенной АС:

• определение политики безопасности;

• проектирование модели АС;

• разработка кода АС;

• обеспечение гарантий соответствия реализации заданной политике безопас-ности.

 

СПИСОК ЛИТЕРАТУРЫ

 

1. Барсуков B.C. Обеспечение информационной безопасности/Яехнологии элек­тронных коммуникаций. Т.63.-М.: Эко-Трендз Ко, 1996.

2. Березин Б.В., Дорошкевич П. В. Цифровая подпись на основе традиционной криптографии. II Защита информации.-1992.- № 2.

3. ВасипецВ.И., Голованов В. Н., Самотуга В. А. Практика обеспечения инфор­мационной безопасности акционерного общества // Конфидент. 4'95.

4. Варфоломеев А.А., Пеленицин М. Б. Методы криптографии и их применение в банковских технологиях, -М., МИФИ, 1995.

5. Водолазкий В.В, Коммерческие системы шифрования: основные алгоритмы и их реализация // Монитор. 5-7.92, 8.92, 6.93.

6. Гайкович В.Ю., Першин А.Ю. Безопасность электронных банковских систем -М.: Компания "Единая Европа", 1994.

7. Гроувер Д. и др. Защита программного обеспечения: Пер. с англ.-М.: Мир, 1992.

8. Жельников В. Криптография от папируса до компьютера.- М.: ABF, 1996.

9. Клопов В.Д., Мотуз О.В. Основы компьютерной стеганографии // Конфидент.-4'97.

10. ЛипаевВ.В. Программно-технологическая безопасность информационных сис­тем // Информационный бюллетень Jei info.-1997. № 6/7.

11. Мафтик С. Механизмы защиты в сетях.-М.: Мир, 1993.

12. Мельников В. В. Защита информации в компьютерных системах-М.: Финансы и статистика-Электроинформ, 1997.

13. Мур Дж.Х. Несостоятельность протоколов криптосистем: Пер. с англ.// ТИИ-ЭР.-1938.-Т.76, N95.

14. Правиков Д.И. Применение циклического контрольного кода // Библиотека ин­формационной технологии/Сб. ст. под ред. Г.Р.Громова.-М.: ИнфоАрт, 1992.-Вып.5.

15. Правиков Д.И. Разработка и исследование методов создания корректных опе­рационных систем реального времени: Дис. канд. тех. науи.-М., 1994.

16. Прокофьев И.В., ШрамковИ.Г, Щербаков А. Ю. Введение в теоретические основы компьютерной безопасности - М.: Издательство МГИЭМ, 1998.

17. РасторгуевС.П. Программные методы защиты информации в компьютерах и сетях.-М.: "Яхтсмен", 1993.

18. Ронин Р. Своя разведка, - Минск: Харвест, 1997.

19. Сапомаа А. Криптография с открытым ключом: Пер. с англ.-М.: "Мир", 1996-

20. Симмонс Г.Дж. Обзор методов аутентификации информации: Пер. с англ.// ТИИЭР.-1988.-Т.76, N25.

21. Спесивцев А.В. и др. Защита информации в персональных ЭВМ.-М.: Радио и связь, 1992.

22. Щербаков А.Ю. Разрушающие программные воздействия.-М.: Эдэль, 1993-

23. Организация и современные методы защиты информации-М.: Концерн "Банковский деловой центр", 1993.

24. Гостехкомиссия России, Руководящий документ: Защита от несанкциониро­ванного доступа к информации. Термины и определения.-М.: Военное изда­тельство, 1992.

25. Clark D., Wilson D. A comparison of Commercial and Military Computer Security Policies// Proce. of the 1987 IEEE Symposium on Security and Privacy.- Oakland, Cal., 1987.

26. Saltzer J., ScrtroederM.D. The protection of Information in Computer Systems// Proce. of the IEEE.-September1975.-63(9):1278-!3Q8.

Порядок выполнения работы

1.Ознакомиться с методологией построения систем защиты информации в АС.

2.Выполнить практическое задание.

3.Ответить на контрольные вопросы.

 

3. Практические задания

1. Разработать интерфейс пользователя «ПОСТРОЕНИЕ СИСТЕМ ЗАЩИТЫ ОТ УГРОЗЫ НАРУШЕНИЯ КОНФИДЕНЦИАЛЬНОСТИ ИНФОРМАЦИИ».

2. Разработать интерфейс пользователя «ПОСТРОЕНИЕ СИСТЕМ ЗАЩИТЫ ОТ УГРОЗЫ НАРУШЕНИЯ ЦЕЛОСТНОСТИ ИНФОРМАЦИИ».

3. Разработать интерфейс пользователя «ПОСТРОЕНИЕ СИСТЕМ ЗАЩИТЫ ОТ УГРОЗЫ ОТКАЗА ДОСТУПА К ИНФОРМАЦИИ».

4. Разработать интерфейс пользователя «ПОСТРОЕНИЕ СИСТЕМ ЗАЩИТЫ ОТ УГРОЗЫ РАСКРЫТИЯ ПАРАМЕТРОВ ИНФОРМАЦИОННОЙ СИСТЕМЫ»

5. Разработать интерфейс пользователя «МЕТОДОЛОГИЯ ПОСТРОЕНИЯ ЗАЩИЩЕННЫХ АС».

 

4. Контрольные вопросы

1) Описать порядок действий злоумышленника с целью получения доступа к информации на машинном носителе.

2) Что такое учетная запись пользователя?

3) Перечислить требования к СКЗИ.

4) Что такое корректное использование МРКФ?

5) Назвать правило Е2 модели Кларка-Вилсона.