КЛОС – это технология и семейство встраиваемых операционных систем с поддержкой многоядерности, с повышенными требованиями к безопасности (КТ-178C) и защищённости (РБПО). В КЛОС обеспечивается пространственная (по памяти) и временнáя (по гарантиям времени отклика) изоляция функционального и системного программного обеспечения. Накладные расходы со стороны ОСРВ минимизированы за счёт статического конфигурирования памяти и непериодических таймеров с квантованием. В статье кратко описывается история работ по созданию операционных систем на основе микроядерного подхода, которые были начаты еще под руководством академика В.П Иванникова в 70-е годы 20-го века и развитие, которое они получили в настоящее время. Более подробно описываются основные архитектурные решения, использованные в версиях КЛОС, которые разрабатываются в ИСП РАН для систем аэрокосмической техники в последние десять лет.

В статье дается обзор существующих работ по использованию языковых моделей (Large Language Models, LLM) для автоматизации построения формальных доказательств в системе Isabelle. Рассматриваются различные уровни взаимодействия пользователей и LLM с системой доказательства. Для каждого уровня рассматриваются преимущества и недостатки практического использования в ходе построения формальных доказательств пользователем, а также возможности автоматизации процесса доказательства с помощью LLM. На основе обзора предлагаются способы улучшения средств использования LLM в системе Isabelle.

В статье исследуются проблемы внедрения технологий верификации программных систем ответственного назначения, в частности, средств защиты информации, на основе формальных методов разработки и верификации программ. Обосновывается выбор метода динамической верификации при верификации средств защиты информации операционных систем общего назначения, где на средства защиты информации возлагается контроль предоставления доступом к информационным объектам, таким как файлы, директории, пользовательские процессы и др. В качестве примера реализации рекомендаций ГОСТ Р 59453.4-2025 «Защита информации. Формальная модель управления доступом. Часть 4. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом» описывается инструмент АНИС. Рассматривается вопрос об ограничения на язык описания формальных моделей управления доступом для его использования в технологии динамической верификации, а также другие вопросы, которые важны для обеспечения требований использования инструмента в практике верификации и сертификации средств защиты информации.

В условиях промышленного производства сбор репрезентативных данных о дефектах печатных плат затруднён, что делает методы контролируемого обучения малоприменимыми. В данной работе исследуется альтернативный подход – одноклассовое обнаружение аномалий на основе β-вариационного автоэнкодера (β-VAE), при котором модель обучается исключительно на изображениях бездефектных плат. Основной фокус работы – анализ влияния неоднородности данных на качество детекции. Эксперименты на наборе данных с четырьмя типами печатных плат показали, что обучение отдельной модели для каждого типа платы позволяет достичь высокого качества (ROC-AUC до 0.98). В то же время, попытка создать универсальную модель для всех типов плат приводит к резкому падению эффективности (ROC-AUC < 0.69), что свидетельствует о критическом влиянии вариативности топологии. Визуализация латентного пространства с помощью t-SNE подтверждает, что оптимальный параметр β способствует лучшему разделению нормальных и аномальных образцов. Наибольшую практическую ценность демонстрирует специализированная свёрточная архитектура
β-CVAE, показавшая конкурентные результаты при значительно меньших вычислительных затратах по сравнению с современными методами.

Наряду с производительностью и площадью энергопотребление является важнейшей характеристикой интегральных схем. В последнее время были предложены методы снижения энергопотребления на разных этапах проектирования: от создания RTL-модели (множественные домены питания, стробирование тактовых сигналов и другие техники) до применения специальных технологических библиотек (в том числе основанных на обратимой логике). В данной работе предложен практический подход к оптимизации энергопотребления микросхем на этапе логического синтеза, а именно на этапе технологически независимой оптимизации. Подход состоит из трех шагов, на каждом из которых совершаются эквивалентные преобразования комбинационных схем. Первый шаг нацелен на сокращение количества логических вентилей и реализуется с помощью итеративной замены подсхем. Второй и третий шаги минимизируют переключательную активность: на втором шаге для этого используется ресинтез подсхем, а на третьем – реструктуризация (балансировка). Экспериментальный анализ показывает, что предложенный подход снижает энергопотребление, о чем свидетельствуют результаты оценки схем после технологического отображения.

В данной статье мы фокусируемся на проблеме технологического отображения, как этапа логического синтеза цифровых СБИС. В основе подхода лежит сопоставление частей исходной логической схемы и элементов технологической библиотеки по таблицам истинности (т.н. Boolean matching). Особенностью предлагаемого подхода является возможность выбора стратегии оптимизации (площадь – как сумма площадей экземпляров технологических ячеек, задержка – как длина критического пути в схеме, потребляемая отображенной схемой мощность – как сумма статического и динамического потребления выбранных технологических ячеек) при удовлетворении ограничений на два других параметра. Подход реализован в инструменте Utopia EDA, распространяемом по лицензии Apache 2.0. В работе показаны результаты проведенных экспериментов над тридцатью одной RTL-моделью, реализованных на языках Verilog/SystemVerilog, с использованием САПР OpenLane. Эксперименты показали, что реализация достижения целевой стратегии в рамках нашего подхода позволяет в большинстве случаев в стратегиях «площадь» и «энергопотребление» достичь результаты лучшие по целевой характеристике, чем достигает ПО Yosys, входящее в САПР OpenLane в качестве средства логического синтеза и технологического отображения. Случай стратегии «задержка» показывает направление дальнейших работ.

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

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

Программно-конфигурируемые сети представляют собой современный подход к управлению сетевыми ресурсами, обеспечивающий гибкость и масштабируемость. Однако их централизованная архитектура делает их уязвимыми для различных типов атак, включая распределенные атаки на отказ в обслуживании. Такие атаки могут привести к значительным финансовым и операционным потерям, что подчеркивает необходимость разработки эффективных методов их обнаружения и предотвращения. В статье рассматриваются методы машинного обучения для противодействия DDoS-атакам в программно-конфигурируемых сетях. Исследование включает анализ атак, с использованием протоколов TCP, ICMP и UDP. Для обнаружения аномалий были применены модели машинного обучения, такие как k-ближайших соседей, деревья решений и вероятностные нейронные сети. Особое внимание уделено борьбе с переобучением с использованием методов кросс-валидации и метода главных компонент. В работе предлагаются сценарии обнаружения и классификации DDoS-атак в программно-конфигурируемых сетях использованием машинного обучения, а также оценка их точности. Результаты исследования помогут оценить эффективность выбранных моделей, на основе метрик F-меры, точности и полноты.

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

Большие языковые модели (LLM) существенно продвинули задачи генерации кода, сделав возможным перевод естественного языка в программный код. Однако эффективность этих моделей в значительной степени зависит от промпт-инжиниринга - практики конструирования входных запросов, которые направляют поведение модели. Хотя предыдущие обзоры рассматривали промпт-инжиниринг в общих приложениях NLP, они дают ограниченное понимание его роли в генерации кода. В данном обзоре мы анализируем 19 стратегий промпт-инжиниринга, специально разработанных для синтеза программ. Мы вводим функциональную таксономию, разделяющую эти стратегии на простые и сложные, а также предлагаем основанную на штрафах оценочную рамку, количественно описывающую компромисс между качеством модели и потреблением ресурсов. Наш анализ объединяет разрозненные результаты, выявляет новые закономерности и предоставляет практические рекомендации специалистам, стремящимся оптимизировать генерацию кода с использованием LLM. Эта работа закладывает основу для будущих исследований адаптивных и экономичных методов построения промптов в синтезе программ.

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

Недавно появившиеся трёхмерные гауссовы сплэтинги (3D Gaussian Splatting) привлекли внимание огромного количества исследователей и имеют потенциал стать одним из основных подходов к реалистичному рендерингу трехмерных сцен. Работа посвящена обзору современных методов и технологий гауссова сплэтинга, который, как мы надеемся, позволит исследователям и практикам быстрее освоиться в этой новой и стремительно развивающейся дисциплине компьютерной графики. Краткий экскурс в историю гауссовых сплэтингов, а также анализ недостатков оригинальных методов помогают лучше разобраться в особенностях современных методов, которые в работе систематизированы по прикладным задачам и основным принципам их решения.

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