By this author

SCENARIO OF INFORMATION FLOW ANALYSIS IMPLEMENTATION IN PL/SQL PROGRAM UNITS WITH PLIF PLATFORM

Issue number 4 from 17.09.2025

Формальное доказательство эффективности реализуемых мер защиты и безопасности вычислений (обработки информации) является важнейшим условием доверия к критическим информационным системам. Важно понимать, что при построении таких систем формальная проверка безопасности должна применяться на всех инфраструктурных уровнях (от физического до прикладного). В настоящее время на практике проблемой остается формальная проверка безопасности вычислений на прикладном уровне, требующая сложной разметки элементов среды вычислений. Для решения данной задачи традиционно используются методы, в основе которых лежит контроль информационных потоков (КИП). В отличие от методов на основе управления доступом, нашедших широкое практическое применение в операционных системах (ОС) и системах управления базами данных (СУБД), КИП в программном обеспечении на практике применяется весьма ограниченно и в основном сводится к анализу помеченных данных – Taint Tracking. В работе приводится вариант реализации КИП в программных блоках PL/SQL с использованием платформы PLIF. Кроме того, описана общая схема проверки безопасности вычислений в приложениях уровня предприятия, работающих с реляционными базами данных. Преимуществом подхода можно считать явное разделение функций разработчиков программного обеспечения и аналитиков безопасности.

18 0

Description of Paralocks language semantics in TLA+

Issue number 1 from 17.09.2025

Одним из основных аспектов реализации контроля информационных потоков в программном обеспечении является язык описания политик безопасности или меток. Важно, чтобы такой язык позволял формировать политики безопасности элементов среды вычислений на основе правил управления доступом системного уровня. Соответственно язык должен быть достаточно гибким, поскольку на системном уровне могут использоваться разные механизмы: ролевое, мандатное управление доступом и др. Кроме того, в приложении могут действовать некоторые дополнительные ограничения. Наконец, желательно, чтобы язык позволял естественным образом учитывать возможность деклассификации данных (контролируемого раскрытия) в процессе вычислений. Одним из таких языков является Paralocks. Работа посвящена реализации семантики несколько упрощенной версии этого языка с использованием TLA+. Paralocks является языковой частью разработанной с участием автора платформы анализа информационных потоков в хранимых программных блоках баз данных PLIF. Приводятся доказательства свойств заданного отношения частичного порядка и решетки, построенной на основе множества всех возможных политик безопасности.

15 0