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

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

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

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

20.03.2017, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28