Объектно-функциональная верификация информационной безопасности распределенных автоматизированных информационных систем таможенных органов - Автореферат
Формализация проблемы обеспечения безопасности информации в распределенных автоматизированных информационных системах с мультикаскадной моделью жизненного цикла. Методы верификации формальной спецификации системы обеспечения безопасности информации.
Аннотация к работе
В их работах разработана концепция защиты информации, обоснованы принципы реализации управляемых процессов обеспечения безопасности информации и принципы построения систем защиты информации объектов информатизации и электронных документов на основе построения изолированной программной среды с использованием программно-аппаратных средств защиты информации, рассмотрены теоретические аспекты и методология организации криптографической защиты информации, развита технология создания информационно-безопасного программного обеспечения в условиях наличия непреднамеренных и намеренных несанкционированных включений - закладок, а также сформулированы основные модели угроз и нарушителей технологической и эксплуатационной безопасности информации. В этих условиях повысить эффективность обеспечения безопасности информации возможно за счет применения методов формализации спецификации системы обеспечения безопасности информации (СОБИ) и ее последующей верификации на этапах проектирования (модернизации) и эксплуатации РАИС. Научная значимость диссертации состоит в развитии теории обеспечения безопасности информации в части разработки моделей, методов и методик формализации спецификации СОБИ РАИС, характеризуемых мультикаскадной спиралевидной моделью жизненного цикла, и последующей ее верификации как на этапе проектирования (разработки, модернизации) РАИС, так и на этапе ее эксплуатации. Результаты диссертационных исследований использовались при непосредственном участии и под руководством автора для разработки целого ряда РАИС таможенных органов, основными из которых являются Система ведомственных удостоверяющих центров таможенных органов (СВУЦТО); Автоматизированная система внешнего доступа таможенных органов (АСВД ТО); Система обеспечения безопасности информации Единой автоматизированной информационной системы таможенных органов (СОБИ ЕАИС ТО). Временной алгебраической сетью Петри называется кортеж S=, где Р={р1,…,pn} и F={f1,…,fm} - конечное множество позиций типа «р» (LIFO, «last in, first out») и типа «f» (FIFO, «first in, first out») соответственно; T={t1,…,tr} - конечное множество переходов; А={а,b,…} - конечный алфавит; - отображение, помечающее дуги, соединяющие позиции с переходами и переходы с позициями; D - вектор с временными параметрами сети, определяющий длительности (задержки) срабатывания переходов; Q - вектор, определяющий активизированные в переходы сети, элементы вектора принимают значения 0 или 1 (переход не выполняется или выполняется); Н - вектор, определяющий время инициализации (активизации) выполнения переходов; ? - время функционирования сети; M: PEF ® A и M0: PEF ® A - текущая и начальная маркировка позиций.