Тип работы:
 Предмет:
 Язык работы:


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

Работа №130630

Тип работы

Магистерская диссертация

Предмет

программирование

Объем работы36
Год сдачи2017
Стоимость5600 руб.
ПУБЛИКУЕТСЯ ВПЕРВЫЕ
Просмотрено
30
Не подходит работа?

Узнай цену на написание


Введение 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


В последнее время происходит стремительный рост количества устройств, подключаемых к Интернет. Взаимодействие между этими устройствами осуществляется
с использованием различных протоколов. В зависимости от целей и потребностей
пользователей Интернет-устройств формулируются различные требования к таким
протоколам. Одно из важных требований является обеспечение конфиденциальности и целостности пользовательских данных. Например, при оплате онлайн-покупок
банковской картой покупатель хочет быть уверен в том, что данные его карты не
попадут к злоумышленникам, а банк получит именно те данные, которые были введены пользователем. Безопасность соединения таких Интернет-устройств зависит от
используемых криптографических протоколов и кода Веб-приложений, который чаще всего создается на 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.


[1] Chlipala Adam. Certified programming with dependent types. — 2016.
[2] Cedric Fournet Nikhil Swamy Juan Chen Pierre-Evariste Dagand Pierre-Yves Strub Ben Livshits. Fully Abstract Compilation to JavaScript // ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013. — ACM, 2013. — P. 371-384. — URL: https://www.microsoft.com/en-us/research/ publication/fully-abstract-compilation-to-javascript/.
[3] Dierks T., Rescorla E. The Transport Layer Security (TLS) Protocol Version 1.2.— 2008. — URL: https://tools.ietf.org/html/rfc5246.
[4] F* Tutorial. — URL: https://www.fstar-lang.org/tutorial/.
[5] Gardner Philippa Anne, Maffeis Sergio, Smith Gareth David. Towards a Program Logic for JavaScript // Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. — POPL ’12. — ACM, 2012. — P. 31-44. - URL: http://doi.acm.org/10.1145/2103656.2103663.
[6] Goal question metric (gqm) approach / Rini Van Solingen, Vic Basili, Gianluigi Caldiera, H Dieter Rombach // Encyclopedia of software engineering. — 2002.
[7] Letouzey Pierre. Extraction in Coq: An Overview // Logic and Theory of Algorithms: 4th Conference on Computability in Europe, CiE 2008, Athens, Greece, June 15-20, 2008 Proceedings. — 2008. — P. 359-369. — URL: http://dx.doi.org/10.1007/ 978-3-540-69407-6_39.
[8] Nir Y. ChaCha20 and Poly1305 for IETF Protocols.- 2015.- URL: https:// tools.ietf.org/html/rfc7539.
[9] Абстрактное синтаксическое дерево программ на Flow.— URL: https:// github.com/facebook/flow/blob/master/src/parser/ast.ml.
[10] Компиляторы. Принципы, технологии и инструментарий / А.В. Ахо, М.С. Лам, Р. Сети, Д. Д. Ульман. — Вильямс, 2016.
[11] Плагин для преобразования export/import-стиля в exports/require-
стиль. — URL: https://www.npmjs.com/package/
babel-plugin-transform-flow-strip-types.
[12] Плагин для удаления типов в JavaScript-программе.— URL: https://www. npmjs.com/package/babel-plugin-transform-flow- strip-types.
[13] Платформа Node.js. — URL: https://nodejs.org/en/.
[14] Рейтинг топ-10 языков программирования, используемых в веб-разработке.—
URL: http://www.rswebsols.com/tutorials/programming/
top-10-programming-languages-web-development.
[15] Репозиторий проекта F*. — URL: https://github.com/FStarLang/FStar/.
[16] Репозиторий проекта HACL*.— URL: https://github.com/mitls/ hacl-star.
[17] Репозиторий проекта KreMLin.— URL: https://github.com/FStarLang/ kremlin.
[18] Репозиторий проекта js-chacha20.— URL: https://github.com/thesimj/ js-chacha20.
[19] Сайт криптографической библиотеки OpenSSL.— URL: https://www. openssl.org/.
[20] Сайт проекта Agda. — URL: http://wiki.portal.chalmers.se/agda/ pmwiki.php.
[21] Сайт проекта BuckleScript. — URL: https://bloomberg.github.io/ bucklescript/.
[22] Сайт проекта Coq. — URL: https://coq.inria.fr/.
[23] Сайт проекта Dafny. — URL: https://github.com/Microsoft/dafny.
[24] Сайт проекта Everest. — URL: https://project-everest.github.io/.
[25] Сайт проекта F*. — URL: https://www.fstar-lang.org/.
[26] Сайт проекта Flow. — URL: https://flow.org/en/.
[27] Сайт проекта Idris. — URL: http://www.idris-lang.org/.
[28] Сайт проекта Vale. — URL: https://github.com/project-everest/vale.
[29] Сайт проекта Web Assembly. — URL: http://webassembly.org/.
[30] Сайт проекта Z3. — URL: http://z3.codeplex.com/.
[31] Сайт проекта js_of_ocaml. — URL: http://ocsigen.org/js_of_ocaml/.
[32] Сайт проекта miTLS. — URL: https://mitls.org/.
[33] Спецификация языка ECMAScript 6.— URL: http://www.
ecma-international.org/publications/standards/Ecma-262.htm.
[34] Список языков программирования, которые транслируются в JavaScript. —
URL: https://github.com/jashkenas/coffeescript/wiki/
list-of-languages-that-compile-to-js.
[35] Сравнение инструмента Flow с языком TypeScript.— URL: http:// djcordhose.github.io/flow-vs-typescript/.

Работу высылаем на протяжении 30 минут после оплаты.




©2025 Cервис помощи студентам в выполнении работ
.