Preview

Труды Института системного программирования РАН

Расширенный поиск

Подход к реализации системы верифицированного исполнения программного кода

https://doi.org/10.15514/ISPRAS-2017-29(6)-1

Аннотация

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

Об авторах

А. В. Козачок
Академия Федеральной службы охраны Российской федерации
Россия


Е. В. Кочетков
Академия Федеральной службы охраны Российской федерации
Россия


Список литературы

1. Указ Президента Российской Федерации от 05.12.2016 № 646 «Об утверждении Доктрины информационной безопасности Российской Федерации».

2. Гарбук С. В., Комаров А. А., Салов Е. И. Обзор инцидентов информационной безопасности АСУТП зарубежных государств: Аналитический отчет. ЗАЩИТА ИНФОРМАЦИИ. ИНСАЙД, вып. 6, 2010 г., стр. 50-58.

3. Яремчук С. APT: реальность или паранойя? Системный администратор, вып. 7-8, 2012 г., стр. 52-56.

4. Довголенко А.А. Социальная инженерия в сети интернет. Информационная безопасность и вопросы профилактики киберэкстремизма среди молодежи Материалы внутривузовской конференции. Под редакцией Г.Н. Чусавитиной, Е.В. Черновой, О.Л. Колобовой, Сборник материалов, 2015 г., стр. 183-191, Магнитогорский государственный технический университет

5. им. Г.И. Носова (Магнитогорск)

6. Козачок А.В. Распознавание вредоносного программного обеспечения на основе скрытых Марковских моделей. Диссертация на соискание ученой степени кандидата технических наук. Воронежский государственный технический университет. Орел, 2012, 209 стр.

7. Козачок А.В., Кочетков Е.В. Обоснование возможности применения верификации программ для обнаружения вредоносного кода. Вопросы кибербезопасности, вып. 3, 2016 г., стр. 25-32.

8. Cimitile A. et al. Model checking for mobile Android malware evolution. Formal Methods in Software Engineering (FormaliSE), 2017 IEEE. ACM 5th International FME Workshop on., 2017, pp. 24-30, IEEE

9. Козачок А.В., Кочетков Е.В. Формальная модель функционирования процесса в операционной системе. Труды СПИИРАН, вып. 2, 2017 г., стр. 78-96.

10. Kozachok A., Bochkov M., Lai Minh T., Kochetkov E. First order logic for program code functional requirements description. Вопросы кибербезопасности, вып. 3, 2017 г., стр. 2-7.

11. Jesse Hertz. Project Triforce: Run AFL on Everything! (online) Доступно по ссылке: https://www.nccgroup.trust/us/about-us/newsroom-and-events/blog/2016/june/projecttri force-run-afl-on-everything/, 01.11.17

12. Институт системного программирования им. В.П. Иванникова РАН. Репозиторий исходного кода эмулятора «Qemu». (online). Доступно по ссылке: https://github.com/ispras/qemu, 09.10.2017

13. Documentation/QMP – QEMU. QEMU Machine Protocol. Доступно по ссылке: https://wiki.qemu.org/Documentation/QMP, 01.11.17


Рецензия

Для цитирования:


Козачок А.В., Кочетков Е.В. Подход к реализации системы верифицированного исполнения программного кода. Труды Института системного программирования РАН. 2017;29(6):7-24. https://doi.org/10.15514/ISPRAS-2017-29(6)-1

For citation:


Kozachok A.V., Kochetkov E.V. Verified program code execution system prototype. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(6):7-24. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(6)-1



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)