RUS ENG

Системы разделения секрета

А. Абрамов, руководитель - проф. Е.А. Крук

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

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

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

Символьные алгоритмы построения автоматов Бюхи по формулам линейной темпоральной логики

A.Беляев, руководитель - ст. преп. И.В. Шошмина

Трансляция формул линейной темпоральной логики (LTL) в автомат Бюхи является одним из основных этапов метода формальной верификации model checking (проверка модели) с помощью так называемого “автоматного подхода”.

“Автоматный подход” к верификации программ оказался очень эффективным, но он существенно зависит от алгоритма преобразования LTL-формулы в автомат Бюхи. Сложность алгоритма верификации линейно зависит от числа состояний модели проверяемой системы (структуры Крипке), но экспоненциально зависит от числа подформул LTL-формулы. Именно этим объясняется интерес исследователей к разработке алгоритмов трансляции. До сих пор проблема построения эффективных алгоритмов преобразования LTL формул в автоматы Бюхи является актуальной и интенсивно обсуждается в литературе. В настоящей работе рассматриваются два алгоритма, реализующих этот важный этап верификации.

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

        Предложенные в работе алгоритмы показали высокую производительность. На некоторых классах формул скорость построения автомата Бюхи предложенным символьным алгоритмом превосходит скорость приведенного в литературе явного алгоритма LTL2BA в несколько тысяч раз.

OpenMVL – открытая научно-исследовательская среда моделирования сложных динамических систем

А. Исаков, руководитель - проф.  Ю.Б. Сениченков

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

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

В качестве базового подхода к построению создаваемого  программного  средства  выбирается  подход к разработке создателей пакета OpenModelica.

В пакете OpenMVL реализованы выбранные механизмы, позволяющие проводить все этапы компьютерного моделирования (от обработки пользовательского описания до проведения численного эксперимента). Сейчас пакет может быть использован для моделирования изолированных непрерывных и гибридных систем, однако в дальнейшем планируется реализовать все возможности языка MVL.