📄Работа №130630
Тема: Компиляция сертифицированных F*-программ в робастные Web-приложения
Тип работы
Магистерская диссертация
Предмет
программирование
Объем:
36 листов
Год:
2017
Просмотров:
70
5600
руб.
🛒 Купить работу
Не подходит эта работа?
Закажите новую по вашим требованиям
Узнать цену на написание
Закажите новую по вашим требованиям
Представленный материал является образцом учебного исследования, примером структуры и содержания учебного исследования по заявленной теме. Размещён исключительно в информационных и ознакомительных целях.
Workspay.ru оказывает информационные услуги по сбору, обработке и структурированию материалов в соответствии с требованиями заказчика.
Размещение материала не означает публикацию произведения впервые и не предполагает передачу исключительных авторских прав третьим лицам.
Материал не предназначен для дословной сдачи в образовательные организации и требует самостоятельной переработки с соблюдением законодательства Российской Федерации об авторском праве и принципов академической добросовестности.
Авторские права на исходные материалы принадлежат их законным правообладателям. В случае возникновения вопросов, связанных с размещённым материалом, просим направить обращение через форму обратной связи.
Настоящий учебно-методический информационный материал размещён в ознакомительных и исследовательских целях и представляет собой пример учебного исследования. Не является готовым научным трудом и требует самостоятельной переработки.
📋 Содержание
Введение 4
1. Постановка задачи 6
2. Обзор 7
2.1. Язык F* 7
2.2. Особенности языка JavaScript 10
2.3. Инструмент Flow 11
2.4. Инструменты трансляции программ на OCaml в JavaScript-приложения 12
2.5. Проект HACL* 14
3. Правила трансляции с языка F* на JavaScript 15
3.1. Описание подхода 15
3.2. Правила трансляции 16
4. Архитектура инструмента и детали реализации 26
4.1. Архитектура инструмента для компиляции F*-программ в робастные
Веб-приложения 26
4.2. Процесс построения JavaScript-приложения из F*-программы 27
4.3. Работа с библиотечными функциями 27
4.4. Взаимодействие с модулями 28
5. Экспериментальное исследование 29
Заключение 33
Список литературы 34
1. Постановка задачи 6
2. Обзор 7
2.1. Язык F* 7
2.2. Особенности языка JavaScript 10
2.3. Инструмент Flow 11
2.4. Инструменты трансляции программ на OCaml в JavaScript-приложения 12
2.5. Проект HACL* 14
3. Правила трансляции с языка F* на JavaScript 15
3.1. Описание подхода 15
3.2. Правила трансляции 16
4. Архитектура инструмента и детали реализации 26
4.1. Архитектура инструмента для компиляции F*-программ в робастные
Веб-приложения 26
4.2. Процесс построения JavaScript-приложения из F*-программы 27
4.3. Работа с библиотечными функциями 27
4.4. Взаимодействие с модулями 28
5. Экспериментальное исследование 29
Заключение 33
Список литературы 34
📖 Введение
В последнее время происходит стремительный рост количества устройств, подключаемых к Интернет. Взаимодействие между этими устройствами осуществляется
с использованием различных протоколов. В зависимости от целей и потребностей
пользователей Интернет-устройств формулируются различные требования к таким
протоколам. Одно из важных требований является обеспечение конфиденциальности и целостности пользовательских данных. Например, при оплате онлайн-покупок
банковской картой покупатель хочет быть уверен в том, что данные его карты не
попадут к злоумышленникам, а банк получит именно те данные, которые были введены пользователем. Безопасность соединения таких Интернет-устройств зависит от
используемых криптографических протоколов и кода Веб-приложений, который чаще всего создается на JavaScript [5]. Поэтому необходимо гарантировать безопасность
используемых протоколов и Веб-приложений, а для последних еще и робастность
(robustness). Веб-приложение является робастным, если оно продолжает работу даже
при неверных входных данных, а не завершается аварийно.
Для работы Веб-приложений широко используется криптографический протокол
Transport Layer Security (TLS) [3], который обеспечивает защищенную передачу данных. Для установки соединения между клиентом и сервером протокол сначала выполняет процедуру подтверждения сеанса связи, которая включает в себя согласование используемых алгоритмов шифрования и хэш-функций, валидацию сертификата
сервера. После этого протокол устанавливает безопасное соединение, которое обеспечивает конфиденциальность передаваемых данных. Для сохранения целостности и
аутентификации сообщений используются так называемые коды аутентификации —
дополнительная информация, получаемая на основе передаваемых данных и позволяющая доказать, что сообщение не изменилось и не было подделано. Несмотря на
продолжительное время разработки криптографических библиотек (например, библиотека OpenSSL [19] разрабатывается с 1998 года), они остаются подвержены хакерским атакам. При этом многие атаки используют ошибки, допущенные в программном
обеспечении. Например, ставшая известной в 2014 году уязвимость Heartbleed [36] в
криптографической библиотеке OpenSSL позволяла несанкционированное чтение памяти на сервере или на клиенте.
с использованием различных протоколов. В зависимости от целей и потребностей
пользователей Интернет-устройств формулируются различные требования к таким
протоколам. Одно из важных требований является обеспечение конфиденциальности и целостности пользовательских данных. Например, при оплате онлайн-покупок
банковской картой покупатель хочет быть уверен в том, что данные его карты не
попадут к злоумышленникам, а банк получит именно те данные, которые были введены пользователем. Безопасность соединения таких Интернет-устройств зависит от
используемых криптографических протоколов и кода Веб-приложений, который чаще всего создается на JavaScript [5]. Поэтому необходимо гарантировать безопасность
используемых протоколов и Веб-приложений, а для последних еще и робастность
(robustness). Веб-приложение является робастным, если оно продолжает работу даже
при неверных входных данных, а не завершается аварийно.
Для работы Веб-приложений широко используется криптографический протокол
Transport Layer Security (TLS) [3], который обеспечивает защищенную передачу данных. Для установки соединения между клиентом и сервером протокол сначала выполняет процедуру подтверждения сеанса связи, которая включает в себя согласование используемых алгоритмов шифрования и хэш-функций, валидацию сертификата
сервера. После этого протокол устанавливает безопасное соединение, которое обеспечивает конфиденциальность передаваемых данных. Для сохранения целостности и
аутентификации сообщений используются так называемые коды аутентификации —
дополнительная информация, получаемая на основе передаваемых данных и позволяющая доказать, что сообщение не изменилось и не было подделано. Несмотря на
продолжительное время разработки криптографических библиотек (например, библиотека OpenSSL [19] разрабатывается с 1998 года), они остаются подвержены хакерским атакам. При этом многие атаки используют ошибки, допущенные в программном
обеспечении. Например, ставшая известной в 2014 году уязвимость Heartbleed [36] в
криптографической библиотеке OpenSSL позволяла несанкционированное чтение памяти на сервере или на клиенте.
✅ Заключение
При выполнении данной работы были получены следующие результаты:
• сформулированы правила трансляции с языка F* на JavaScript, гарантирующие
сохранение аннотаций типов;
• выполнена реализация предложенного подхода на языке F*. Исходный код реализованного инструмента доступен по ссылке https://github.com/FStarLang/
FStar/tree/polubelova_backends, автор принимал участие под учетной записью polubelova;
• проведено экспериментальное исследование реализованного инструмента на примерах из криптографической библиотеки HACL*.
В дальнейшем планируется добавить возможность компиляции F*-программ в
WebAssembly + JavaScript приложения и доказать корректность такой компиляции.
Также планируется провести апробацию полученного инструмента на криптографической библиотеке HACL*, для которой нужно будет реализовать F*-библиотеки, используемые при верификации программ, на языке JavaScript.
• сформулированы правила трансляции с языка F* на JavaScript, гарантирующие
сохранение аннотаций типов;
• выполнена реализация предложенного подхода на языке F*. Исходный код реализованного инструмента доступен по ссылке https://github.com/FStarLang/
FStar/tree/polubelova_backends, автор принимал участие под учетной записью polubelova;
• проведено экспериментальное исследование реализованного инструмента на примерах из криптографической библиотеки HACL*.
В дальнейшем планируется добавить возможность компиляции F*-программ в
WebAssembly + JavaScript приложения и доказать корректность такой компиляции.
Также планируется провести апробацию полученного инструмента на криптографической библиотеке HACL*, для которой нужно будет реализовать F*-библиотеки, используемые при верификации программ, на языке JavaScript.
ИЛИ
Поиск аналога
📕 Список литературы
🛒 Оформить заказ
⚡ Работу высылаем в течении 5 минут после оплаты.