Для студентов РУТ (МИИТ) по предмету ДругиеКомпиляция сертифицированных F*-программ в робастные Web-приложенияКомпиляция сертифицированных F*-программ в робастные Web-приложения
2024-07-112024-07-11СтудИзба
Курсовая работа: Компиляция сертифицированных F*-программ в робастные Web-приложения
Описание
Оглавление
3
Введение
Для работы Веб-приложений широко используется криптографический протокол Transport Layer Security (TLS) [3], который обеспечивает защищенную передачу дан-ных. Для установки соединения между клиентом и сервером протокол сначала вы-полняет процедуру подтверждения сеанса связи, которая включает в себя согласова-ние используемых алгоритмов шифрования и хэш-функций, валидацию сертификата сервера. После этого протокол устанавливает безопасное соединение, которое обес-печивает конфиденциальность передаваемых данных. Для сохранения целостности и аутентификации сообщений используются так называемые коды аутентификации — дополнительная информация, получаемая на основе передаваемых данных и позво-ляющая доказать, что сообщение не изменилось и не было подделано. Несмотря на продолжительное время разработки криптографических библиотек (например, биб-лиотека OpenSSL [19] разрабатывается с 1998 года), они остаются подвержены хакер-ским атакам. При этом многие атаки используют ошибки, допущенные в программном обеспечении. Например, ставшая
| Введение | 4 | ||
| 1. | Постановка задачи | 6 | |
| 2. | Обзор | 7 | |
| 2.1. | ЯзыкF* ..................................... | 7 | |
| 2.2. | Особенности языка jаvascript . . . . . . . . . . . . . . . . . . . . . . . . . | 10 | |
| 2.3. | Инструмент Flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | 11 | |
| 2.4. | Инструменты трансляции программ на OCaml в jаvascript-приложения | 12 | |
| 2.5. | ПроектHACL*.................................. | 14 | |
| 3. | Правила трансляции с языка F* на jаvascript | 15 | |
| 3.1. | Описаниеподхода................................ | 15 | |
| 3.2. | Правилатрансляции .............................. | 16 | |
| 4. | Архитектура инструмента и детали реализации | 26 | |
| 4.1. | Архитектура инструмента для компиляции F*-программ в робастные | ||
| Веб-приложения................................. | 26 | ||
| 4.2. | Процесс построения jаvascript-приложения из F*-программы . . . . . . | 27 | |
| 4.3. | Работа с библиотечными функциями . . . . . . . . . . . . . . . . . . . . . | 27 | |
| 4.4. | Взаимодействиесмодулями.......................... | 28 | |
| 5. | Экспериментальное исследование | 29 | |
| Заключение | 33 | ||
| Список литературы | 34 | ||
3
Введение
- последнее время происходит стремительный рост количества устройств, под-ключаемых к Интернет. Взаимодействие между этими устройствами осуществляется
- использованием различных протоколов. В зависимости от целей и потребностей пользователей Интернет-устройств формулируются различные требования к таким протоколам. Одно из важных требований является обеспечение конфиденциально-сти и целостности пользовательских данных. Например, при оплате онлайн-покупок банковской картой покупатель хочет быть уверен в том, что данные его карты не попадут к злоумышленникам, а банк получит именно те данные, которые были вве-дены пользователем. Безопасность соединения таких Интернет-устройств зависит от используемых криптографических протоколов и кода Веб-приложений, который ча-ще всего создается на jаvascript [5]. Поэтому необходимо гарантировать безопасность используемых протоколов и Веб-приложений, а для последних еще и робастность (robustness). Веб-приложение является робастным, если оно продолжает работу даже при неверных входных данных, а не завершается аварийно.
Для работы Веб-приложений широко используется криптографический протокол Transport Layer Security (TLS) [3], который обеспечивает защищенную передачу дан-ных. Для установки соединения между клиентом и сервером протокол сначала вы-полняет процедуру подтверждения сеанса связи, которая включает в себя согласова-ние используемых алгоритмов шифрования и хэш-функций, валидацию сертификата сервера. После этого протокол устанавливает безопасное соединение, которое обес-печивает конфиденциальность передаваемых данных. Для сохранения целостности и аутентификации сообщений используются так называемые коды аутентификации — дополнительная информация, получаемая на основе передаваемых данных и позво-ляющая доказать, что сообщение не изменилось и не было подделано. Несмотря на продолжительное время разработки криптографических библиотек (например, биб-лиотека OpenSSL [19] разрабатывается с 1998 года), они остаются подвержены хакер-ским атакам. При этом многие атаки используют ошибки, допущенные в программном обеспечении. Например, ставшая
Характеристики курсовой работы
Предмет
Учебное заведение
РУТ (МИИТ)Семестр
Просмотров
1
Размер
647,5 Kb
Список файлов
Компиляция сертифицированных F*-программ в робастные Web-приложения.doc
Tortuga
11 июля 2024 в 07:41
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
