Понятие корректности или правильности подразумевает соответствие проверяемого объекта некоторому эталонному обьекту или совокупности формализованных эталонных характеристик и правил. Корректность ПО при разработке наиболее полно определяется степенью соответствия предъявляемым к ней формализованным требованиям программной спецификации. В спецификациях отражается совокупность эталонных характеристик, свойств и условий, которым должна соответствовать программа. Основную часть спецификации составляют функциональные критерии и характеристики. Исходной программной спецификацией, которой должна соответствовать программа, является ТЗ.
При отсутствии полностью формализованной спецификации требований в качестве ТЗ, которому должна соответствовать АС и результаты ее функционирования, иногда используются неформализованные представления разработчика, пользователя или заказчика программ. Однако понятие корректности программ по отношению к запросам пользователя или заказчика сопряжено с неопределённостью самого эталона, которому должна соответствовать АС. Для сложных программ всегда существует риск обнаружить их некорректность (по мнению пользователя или заказчика) при формальной корректности относительно спецификаций вследствие неточности самих спецификаций.
TFTDS 9. Формальные методы. TLA+
Традиционный взгляд на спецификацию требований заключается в том, что она представляет собой документ на естественном языке, который является интерфейсом между заказчиком и изготовителем. Хотя подготовке документа может предшествовать некоторое взаимодействие, именно этот документ в значительной степени выступает как «отправная точка» для изготовителя программ.
Таким образом, можно сделать вывод о том, что создание совокупности взаимоувязанных непротиворечивых спецификаций является необходимой базой для обеспечения корректности проектируемой программы. При этом спецификации должны:
• позволять проверять непротиворечивость и полноту требований заказчика;
• служить основой для дальнейшего формализованного проектирования ОС.
Существует несколько подходов к определению спецификаций требований.
Спецификация как описание. Заказчик выдает спецификацию, чтобы изготовители могли снабдить его тем изделием, которое он желает, поэтому заказчик видит этот документ главным образом как описание системы, которую он желал бы иметь. В принципе, в описании должно быть указано, что должна и что не должна делать система.
На практике обычно по умолчанию предполагается, что система должна делать то, что уточняется в спецификации, и не должна делать ничего более. В этом состоит главная проблема с описательной стороной спецификации. Предполагается, что заказчик всегда точно знает всё, что система должна и не должна делать. Более того, в дальнейшем предполагается, что заказчик полностью перенёс это знание в специфицированный документ.
Спецификация как предписание. Изготовитель смотрит на специфицированный документ как на набор составных частей, подлежащих сборке, чтобы разрешить проблему заказчика. Такой предписывающий взгляд обуславливается не только трудностями создания описательного документа (как указывалось выше), но и сведениями, которые умышленно или неумышленно расширяют или ограничивают свободу изготовителя.
Формальные спецификации на примере TLA+
Договорная методология. В рамках «описание заказчика-предписание изготовителю» спецификация рассматривается как формальное разделение между сторонами. Что касается заказчика, то он оговаривает минимально приемлемое, тогда как изготовитель — максимально требуемое. Договор предлагается и принимается при зарождении системы и заканчивается после завершения системы, когда заказчик принимает систему как отвечающую его минимальным требованиям. Во время изготовления системы в принципе не предполагается никаких взаимодействий, даже если изготовитель подозревает, что предписываемое не совсем соответствует тому, что заказчик желает видеть в действительности.
Спецификация как модель. Современные более строгие представления о спецификации трактуют ее как модель системы. При условии, что лежащая в основе модели семантика в достаточной мере обоснована, такая спецификация обеспечивает чёткую формулировку требований.
Соответствующие модели подходят также для автоматизированного контроля целостности и другого прогнозного анализа, который, в частности, обеспечит прекращение разработки системы, в принципе не способной удовлетворить требованиям.
Модели как описание системы имеют следующие отличительные черты по сравнению сдругими способами формального описания:
• хорошее сочетание нисходящего и восходящего подходов к их разработке с возможностью выбора абстрактного описания;
• возможность описания параллельной, распределенной и циклической работы;
• возможность выбора различных формализованных аппаратов для описания систем.
Основное преимущество использования формальной модели заключается в возможности исследования с ее помощью особенностей моделируемой системы. Основывая формальный метод разработки на математической модели и затем исследуя модель, можно выявить такие грани поведения системы, которые в противном случае не были бы очевидны до более поздних стадий.
Так как целевым объектом проектирования является АС, то модель может описывать либо саму АС, либо ее поведение, т.е. внешние проявления функционирования АС. Модель, описывающая поведение АС по сравнению с моделью АС, обладает одним важным преимуществом — она может быть проверена и оценена как исполнителями, так и заказчиками, поскольку заказчики не знают, как должна работать АС, но зато они представляют, что она должна делать. В результате такого моделирования может быть проверена корректность спецификаций относительно исходной постановки задачи, т.е. ТЗ. Кроме того, критерии правильности считаются достаточными при условии, что спецификация представляет собой исчерпывающее описание «внешнего» поведения объекта при всех возможных (или запланированных) ситуациях его использования.
Как было отмечено выше, при разработке АС, особенно ее компонентов, представляющих систему защиты информации, для обеспечения высоких гарантий отсутствия неисправностей и последующего доказательства того, что система функционирует согласно требованиям ТЗ, используются формальные подходы к ее проектированию.
Формальное проектирование алгоритмов базируется, в основном, на языках алгоритмических логик, которые включают высказывание вида
читающееся следующим образом: «если до исполнения оператора S было выполнено условие Q, то после него будет R». Здесь Q называется предусловием, a R — постусловием. Эти языки были изобретены практически одновременно Р.У.Флойдом (1967г.), С.А.Р.Хоаром (1969г.) и учеными польской логической школы (А. Сапьвицкий и др., 1970 г.>. Как предусловие, так и постусловие являются предикатами.
Рассмотрение программ в качестве некоего «преобразователя предикатов» позволяет прямо определить связь между начальными и конечными состояниями без каких-либо ссылок на промежуточные состояния, которые могут возникнуть во время выполнения программы.
Преимущество представления алгоритма в виде преобразователя предикатов состоит в том, что оно дает возможность:
• анализировать алгоритмы как математические обьекты;
• дать формальное описание алгоритма, позволяющее интеллектуально охватить алгоритм;
• синтезировать алгоритмы по представленным спецификациям;
• провести формальное верифицирование алгоритма, т.е. доказать корректность его реализации.
Методология формальной разработки и доказательства корректности алгоритмов в настоящее время хорошо разработана и изложена в целом ряде работ. Вкратце суть этих методов сводится к следующему:
• разработка алгоритма проводится методом последовательной декомпозиции, с разбивкой общей задачи, решаемой алгоритмом, на ряд более мелких подзадач;
• критерием детализации подзадач является возможность их реализации с помощью одной конструкции ветвления или цикла;
• разбиение общей задачи на подзадачи предусматривает формулирование пред- и постусловий для каждой подзадачи с целью их корректного проектирования и дальнейшей верификации.
Для доказательства корректности алгоритма (верификация) формулируется математическая теорема QR, которая затем доказывается. Доказательство теоремы о корректности принято разбивать на две части. Одна часть служит для доказательства того, что рассматриваемый алгоритм вообще может завершить работу (проводится анализ всех циклов). В другой части доказывается корректность постусловия в предположении, что алгоритм завершает работу.
Теория безопасных систем (ТСВ)
Понятие «доверенная вычислительная среда» (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 модели Кларка-Вилсона.
Источник: infopedia.su
Методы доказательства правильности программ
Как известно, универсальные вычислительные машины могут быть запрограммированы для решения самых разнородных задач — в этом заключается одна из основных их особенностей, имеющая огромную практическую ценность. Один и тот же компьютер, в зависимости от того, какая программа находится у него в памяти, способен осуществлять арифметические вычисления, доказывать теоремы и редактировать тексты, управлять ходом эксперимента и создавать проект автомобиля будущего, играть в шахматы и обучать иностранному языку. Однако успешное решение всех этих и многих других задач возможно лишь при том условии, что компьютерные программы не содержат ошибок, которые способны привести к неверным результатам.
Можно сказать, что требование отсутствия ошибок в программном обеспечении совершенно естественно и не нуждается в обосновании. Но как убедиться в том, что ошибки, в самом деле, отсутствуют? Вопрос не так прост, как может показаться на первый взгляд.
К неформальным методам доказательства правильности программ относят отладку и тестирование, которые являются необходимой составляющей на всех этапах процесса программирования, хотя и не решают полностью проблемы правильности. Существенные ошибки легко найти, если использовать соответствующие приемы отладки (контрольные распечатки, трассировки).
Тестирование – процесс выполнения программы с намерением найти ошибку, а не подтвердить правильность программы. Суть его сводится к следующему. Подлежащую проверке программу неоднократно запускают с теми входными данными, относительно которых результат известен заранее. Затем сравнивают полученный машиной результат с ожидаемым. Если во всех случаях тестирования налицо совпадение этих результатов, появляется некоторая уверенность в том, что и последующие вычисления не приведут к ошибочному итогу, т.е. что исходная программа работает правильно.
Лекция 9. Аналитическая проверка корректности программ. Верификация программ
Корректность является статическим свойством программы, поскольку она не зависит от времени (если, конечно, не изменяются цели разработки) и отражает специфику ошибок разработки программ (ошибок проекта и кодирования).
Различают два типа проверки корректности:
· валидация (validation) – установление соответствия между тем, что делает программа, и тем, что нужно Заказчику;
· верификация (verification) – установление соответствия между программой и ее спецификацией.
Определение верификациии симметрично ввиду относительного характера свойства корректности: если программа не соответствует своей спецификации, то либо программа, либо спецификация, либо оба этих объекта содержат ошибки. Перефразируя известное изречение Э.Дейкстры о тестировании программ, можно сказать, что верификация способна доказать отсутствие ошибок в программе, но не всегда доказывает их присутствие.
В отличие от тестирования верификация предполагает аналитическое исследование свойств программы по ее тексту (без выполнения программы). Таким образом, для проведения верификации необходимо построить формально-логическую систему, в которой были бы формально определены свойства корректности программы. Для этих целей наиболее широкое применение получило исчисление предикатов первого порядка, расширенное аксиоматической арифметикой.
Можно сказать, что верификация – это вычисление истинности предикатаот двух аргументов: программы и спецификации. Истинность этого предиката устанавливает свойство корректности программы, если спецификация не содержит ошибок, однако, его ложность, вообще говоря, не означает наличие ошибок в программе, а требует более точного разбора.
Учитывая специфику проявления ошибок в программах в процессе их выполнения на ЭВМ, целесообразно выделить в понятие корректности программы два свойства:
· частичную корректность – удовлетворение внешним (входной и выходной) спецификациям программы при условии завершения выполнения программы;
· завершенность – достижение в процессе выполнения выхода программы при определенных входной спецификацией данных.
Свойство завершенностине является тривиальным для такого объекта, как программа, ввиду возможности циклических и рекурсивных вычислений, а также наличия частично-определенных операций. Случаи, когда свойство завершенности не удовлетворяется, довольно обычны для программ с ошибками, и приводят к заведомо некорректным программам независимо от спецификации выхода.
Каждое из двух выделенных свойств корректности программы может удовлетворяться или не удовлетворяться. Таким образом, можно выделить шесть основных задач анализа корректности программы:
· частичная корректность (при условии завершенности);
· тотальная корректность (частичная корректность и завершенность);
· частичная некорректность (некорректность при условии завершенности);
· некорректность (незавершенность или частичная некорректность).
Разделение свойств частичной корректности и завершенности следует рассматривать как методологический прием, направленный на уменьшение сложности верификации программ.
Рассмотрим формальные постановки задач анализа корректности.
Введем ограничение: будем рассматривать программы, начинающиеся оператором START (первый выполняемый оператор) и заканчивающиеся оператором STOP (последний выполняемый оператор).
Спецификацию программы Prgm будем определять путем приписывания индуктивных утвержденийточкам разреза графа потоков управления программы (точкам между операторами программы). При этом выходу оператора START приписывается входной предикат (предусловие) программы P(x), определяющий множество допустимых значений исходных данных x (x допустимо, если P(x): true), а входу оператора STOP приписывается выходной предикат (постусловие) Q(x,y), определяющий целевую функцию программы (связь между входными и выходными данными программы).
Тогда свойство частичной корректности программы определяется следующей формулой логики предикатов:
PCOR(Prgm, P, Q): «x (P(x) Ù fin(x) Þ Q(x, f(x))),
где fin(x) – предикат завершения программы Prgm, начатой в состоянии x;
f(x) – функция, вычисляемая программой Prgm,
свойство завершенности может быть определено формулой:
FIN(Prgm, P): «x (P(x) Þ fin(x)),
а свойство тотальной корректности формально выражается как одновременное присутствие свойств частичной корректности и завершенности:
TCOR(Prgm, P, Q): «x (P(x) Þ Q(x, f(x)) Ù fin(x)).
Аналогичным образом могут быть формализованы и другие перечисленные выше свойства корректности (записать самостоятельно).
Заметим, что для произвольных программ каждое из этих свойств (завершенность и частичная корректность) является алгоритмически неразрешимым, т.е. не существует алгоритма, позволяющего оценить истинность соответствующих формул логики предикатов. Однако для отдельных классов программ в настоящее время разработаны достаточно эффективные методы верификации, позволяющие вручную или автоматически проводить соответствующие доказательства. Такие методы могут рассматриваться как составная часть процессов разработки и отладки программ, обеспечивая логическую завершенность этих процессов.
Наиболее распространенным методом доказательства частичной корректности программ является метод индуктивных утверждений, предложенный Флойдом. Он позволяет свести доказательство частичной корректности программы к доказательству некоторого конечного числа утверждений, записанных на языке исчислений предикатов первого порядка и имеющих интерпретацию в соответствующей проблемной области.
Рассмотрим метод индуктивных утверждений для программ с конечным множеством простых переменных < x1, x2, … xn >, где n³1, а операторами являются:
· операторы присваивания вида xi:= f (x1, x2, … xn);
· составной оператор вида A; B;
· оператор условного перехода if a(x1, x2, … xn) then L+ else L–,
где L+, L – – метки операторов, которым передается управление;
· начальный оператор START;
· конечный оператор STOP.
Такой состав структурных компонентов вполне достаточен для представления произвольного алгоритма и поэтому не ограничивает общности излагаемого метода.
Установление частичной корректности осуществляется за четыре последовательных шага.
Шаг 1.Разрезание циклов программы
Очевидно, что при выполнении программы для различных исходных данных возможны различные последовательности операторов, начинающиеся оператором START и оканчивающиеся оператором STOP. Назовем такие последовательности трассами вычислений.
Сложность анализа частичной корректности программы разбиением на трассы заключается в том, что при наличии циклов в программе он не может быть выполнен непосредственным перебором всех трасс. Эта сложность может быть преодолена путем включения в граф потока управления программы конечного числа точек, называемых точками разреза, таким образом, что каждый цикл содержит одну такую точку, которая “ разрезает ” циклические пути на два:
· путь через тело цикла;
· путь к выходу из цикла.
Понравилась статья? Добавь ее в закладку (CTRL+D) и не забудь поделиться с друзьями:
Источник: studopedia.ru