В связи с начавшимся процессом внедрения ФСТЭК России «Требований безопасности информации к операционным системам» в работе анализируются пути выполнения требований функциональной компоненты ADV_SPM.1 «Формальная модель политики безопасности», в том числе по определению языка, глубины и детализации представления модели политики безопасности управления доступом и информационными потоками. При этом приводятся предложения по составу основных элементов модели, использованию для ее верификации инструментальных средств. Практическая возможность применения предлагаемых подходов рассматривается на примере представления описания и верификации МРОСЛ ДП-модели, как основы механизма управления доступом в ОССН Astra Linux Special Edition.

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

В статье рассматривается семейство требований доверия к безопасности ADV_SPM «Моделирование политики безопасности», которое определяется стандартом ГОСТ Р ИСО/МЭК 15408-3-2013 «Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности». Обсуждаются задачи, решаемые этим семейством, и вопросы, которые возникают при попытке интерпретировать его требования. На простом примере представляется подход к формализации политик безопасности при помощи языка формальных спецификаций Event-B и инструментов платформы Rodin.

В статье описываются работы, выполненные для поддержки анализа программ на языке Java в статическом анализаторе Svace, разрабатываемом в ИСП РАН. Приводятся методы построения внутреннего представления для анализа Java, включая изменения в компоненте контролируемой сборки, доработки компилятора OpenJDK, трансляцию байткода Java в окончательное представление для анализа. Описываются особенности анализа Java-программ - алгоритм девиртуализации, спецификации методов стандартной библиотеки Java, некоторые специфичные детекторы. Представлены результаты выполнения анализа для исходного кода операционной системы Android 5.

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

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

JetOS - перспективная бортовая операционная система реального времени (ОСРВ), разработка которой в настоящее время ведется в рамках научно-исследовательской работы ГосНИИАС. В статье указаны предпосылки появления JetOS и рассмотрены работы, ведущиеся по направлению создания ОСРВ. ОСРВ разрабатывается в соответствии с DO-178C и ARINC 653, учтена возможность работы с OpenGL SC. В статье приведены аппаратные аспекты создания ОСРВ - поддержка многоядерности, платформонезависимость и другие. Одной из важнейших задач при разработке ОСРВ является получение сертификационного пакета, соответствующего DO-178C, благодаря чему JetOS можно будет применять при создании и модернизации авионики для гражданской авиации.

Задача о нахождении большой "спрятанной" клики в случайном графе и ее аналог для двудольных графов являются объектами рассмотрения в данной заметке.

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