| Наименование РИД |
Программа для проверки корректности контроля доступа в системах больших данных с использованием темпоральной логики
|
| Реферат |
Программа предназначена для проверки корректности контроля
доступа при обработке и хранении больших данных.
Программа может использоваться в системах больших данных.
Функциональные возможности программы: Программа принимает
на вход файл, описывающий пользователей системы больших данных,
включая имена, функциональные роли, подразделения; файл, описывающий
графовую модель системы больших данных в виде списка вершин
фрагментов данных и ребер-направлений обработки данных; файл,
содержащий ограничения для генерации спецификаций. Программа для всех
указанных пользователей генерирует спецификации контроля доступа на
основе временной логики TLA+ с учетом заданных ограничений.
Выполняется
TLC
(explicit-state
model-checker)-верификация
и
результирующая матрица доступа сохраняется в выходную HTML-таблицу,
где отмечены выявленные нарушения безопасности.
|
| Возможные направления использования |
Программа может использоваться для формальной проверки корректности контроля доступа в системе обработки и хранения больших данных с использованием темпоральной логики.
|
| Количество опытных образцов |
1
|
| Количество просмотров |
2
|
| Наличие дополнительных файлов |
False
|
| Использование РИД правообладателем |
False
|
| Внешнее использование РИД |
False
|
| НИОКТР (JSON) |
{}
|
| ИКСИ (JSON) |
[]
|
| ИКСПО (JSON) |
[{"last_status": {"created_date": "2025-12-19T16:56:13.987350+00:00", "registration_number": "825121900051-4", "status": {"name": "Подтверждена"}}, "copyright_protections": [{"protection_way": {"name": "Осуществлена государственная регистрация"}}]}]
|
| ОЭСР (JSON) |
[]
|
| Дата первого статуса |
2025-10-17T08:08:02.202703+00:00
|
| Предполагаемый тип результата |
Программа для ЭВМ
|
| Ожидаемая роль |
Исполнитель
|
| Заказчик |
Российский научный фонд
|
| Руководитель работы |
Зегжда Дмитрий Петрович
|
| Руководитель организации |
Кадиев Исмаил Гаджиевич
|
| Регистрационный номер НИОКТР |
123112000035-0
|
| Последний статус |
Подтверждена, 625110500081-1, 2025-11-05 08:17:34 UTC
|
| ОКПД |
Услуги по проектированию и разработке информационных технологий для прикладных задач и тестированию программного обеспечения
|
| Ключевые слова |
информационная безопасность; граф; большие данные; TLA+; TLC-верификация; спецификация; матрица доступа; темпоральная логика
|
| Исполнители |
ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ АВТОНОМНОЕ ОБРАЗОВАТЕЛЬНОЕ УЧРЕЖДЕНИЕ ВЫСШЕГО ОБРАЗОВАНИЯ "САНКТ-ПЕТЕРБУРГСКИЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ПЕТРА ВЕЛИКОГО"
|
| Авторы |
Калинин Максим Олегович; Полтавцева Мария Анатольевна
|
| Коды тематических рубрик |
50.43.19 - Системы автоматического контроля функционирования сложных систем
|
| OESR |
Автоматизированные системы управления
|
| Приоритеты научно-технического развития |
д) противодействие техногенным, биогенным, социокультурным угрозам, терроризму и экстремистской идеологии, деструктивному иностранному информационно-психологическому воздействию, а также киберугрозам и иным источникам опасности для общества, экономики и государства, укрепление обороноспособности и национальной безопасности страны в условиях роста гибридных угроз;
|
