Comments 3
Звучит как известная цитата - "Современным математикам вообще трудно читать своих предшественников, которые писали: `Петя вымыл руки' там, где просто следовало сказать: `Существует t1 < 0, такое, что образ Петя(t1) точки t1 при естественном отображении t → Петя(t) принадлежит множеству грязноруких и такое t2 из полуинтервала (t1, 0], что образ точки t2 при том же отображении принадлежит дополнению к множеству, о котором шла речь при рассмотрении точки t1.'"
Т.е, совсем непонятно, зачем задачу типа "доказать, что у пользователя не может появиться дополнительное право доступа, которым он не должен обладать" переформулировать в терминах теории множеств. Ведь по сути, для доказательства, нужно все равно обратно вернуться в описание самой системы и использовать понятия самой системы типа "пользователь" или "право доступа", так зачем же дополнительный слой усложнения?
Т.е, совсем непонятно, зачем задачу типа "доказать, что у пользователя не может появиться дополнительное право доступа, которым он не должен обладать" переформулировать в терминах теории множеств
Есть вероятность, что эти требования пролоббированы в ФСТЭК отдельными игроками дабы усложнить жизнь конкурентам. Отсюда сама постановка вашего вопроса не состоятельна. Но!
Исходная мысль формальной верификации в контексте IT вполне академически интересна - построить мат. модель программного объекта, обладающую той или иной логической непротиворечивостью процессов. И уже на ее основе приступать к проектированию и разработке ПО, обладающего исходно требуемыми характеристиками. Встречал упоминания инструмента, который позволяет формировать абстрагированный исходный код и даже отсылки к академическим проектам, где этот подход реализован на практике. Нужно ли упоминать, что экономически это сильно накладнее *-и-в-продакшен? В 2008-2012 ЕС проплатили разработку некоммерческого Eclipse-based IDE для реализации этой идеи (см. "The development of Rodin has been supported by the European Union projects DEPLOY (2008–2012), RODIN (2004–2007), and ADVANCE (2011–2014)"). Его развитие, к слову, не остановлено и сейчас - выходят новые версии, хотя это и похоже больше на багфиксы.
У нас в стране, однако, формальная верификация превратилась большую фикцию.
Здравую идею перевернули с ног на голову. По описанию (а не по реальному объекту или его исходникам) некоего процесса в объекте строится модель и формальными методами доказывается ее (модели) непротиворечивости. Таким образом, имеем построение формальной модели по вербальной модели (описанию той же СЗИ) реального объекта и дальнейшее формулирование выводов об исходном объекте. Это сродни метамоделированию, но совершенно отвязанное от реальности, поскольку сам объект никак не затрагивает. В итоге весь исходный мат. аппарат используется в обратной последовательности. Адепты этого подхода апеллируют к тому, что логика есть мощнейший инструмент доказательства сам по себе. Вот только состоятельность метамодели может быть доказана лишь относительно исходной модели, но не самого объекта. Предположение относительно целей сего фарса я уже высказал.
Далее планирую освятить вопрос
Без привлечения церкви в этом вопросе никак не обойтись?
P.S. Почему вы указываете, что вы PhD, когда вы аспирант? Корректное наименование postgraduate student или Ph.D. student.
Построение и доказательство модели безопасности СЗИ с помощью математического аппарата