Исследовательская группа

Лаборатория языковых инструментов

Компиляция сертифицированных F*-программ в надежные веб-приложения

March 20

Доклад посвящен компиляции сертифицированных F*-программ в надежные (robust) веб-приложения. Будет дан обзор функционального языка программирования F*, ориентированного на верификацию программ и позволяющего доказывать их функциональную корректность и безопасный доступ к памяти. Поскольку данный инструмент позволяет только верифицировать программы, но не исполнять их, то необходим механизм извлечения верифицированного кода в другой левой язык. В качестве примера такого языка взят язык программирования JavaScript, который широко применяется при веб-разработке. В данном докладе будут подробно рассмотрены правила трансляции F*-программ в JavaScript-приложения с сохранением аннотаций типов с целью дополнительной проверки инструментом Flow (type checker для JavaScript) полученной программы. Как иллюстрация будет использоваться проект, посвященный доказательству корректности реализации криптографических протоколов, таких как Transport Layer Security (TLS), с точки зрения их соответствия математической спецификации.

Докладчик: Марина Полубелова