ОСОБЕННОСТИ ПРОГРАММНОЙ АРХИТЕКТУРЫ ЯЗЫКОВОЙ ПЛАТФОРМЫ PLIF ДЛЯ АНАЛИЗА БЕЗОПАСНОСТИ ИНФОРМАЦИОННЫХ ПОТОКОВ В АВТОМАТИЗИРОВАННЫХ СИСТЕМАХ

Алексей А. Тимаков, Михаил М. Фадеев, Илья Г. Рыжов, Александр В. Лысиков

Аннотация


В области формальных моделей безопасности компьютерных систем к настоящему времени выполнен значительный объем исследований. Одним из наиболее важных направлений является контроль информационных потоков в программных средах автоматизированных систем. Соответствующие механизмы сегодня активно исследуются, предпринимаются попытки их внедрения в языковые платформы, предназначенные для создания как системного, так и прикладного программного обеспечения. На данном этапе научной проработки указанное направление можно отнести к академическому, характеризуемому теоретическими изысканиями и появлением множества прототипов. По мнению авторов, основной проблемой использования обозначенных механизмов при создании промышленных автоматизированных систем и включения соответствующих этапов в цикл безопасной разработки является сложность ручного инструментирования программного кода на основе меток безопасности и проверка выявленных нарушений. В работе представлена разработанная технологическая платформа выявления запрещенных информационных потоков в программных блоках систем управления базами данных, предложена общая процедура ее применения, которая предполагает разделение функций разработчиков программного обеспечения и аналитиков информационной безопасности.


Ключевые слова


информационные потоки, контроль информационных потоков, формальная верификация, языковая платформа, политика безопасности.

Полный текст:

PDF

Литература


1. Adam Chlipala. 2015. Ur/Web: A Simple Model for Programming the Web. SIGPLAN Not. 50, 1 (January 2015), р. 153–165. DOI: https://doi.org/10.1145/2775051.2677004.

2. Arden O., George M.D., Liu J., Vikram K., Askarov A. and Myers A.C. Sharing Mobile Code Securely with Information Flow Control. IEEE Symposium on Security and Privacy, San Francisco, CA, USA. 2012,
p. 191–205. DOI: https://doi.org/10.1109/SP.2012.22.

3. Daniel Schoepe, Daniel Hedin, and Andrei Sabelfeld. 2014. SeLINQ: tracking information across application-database boundaries. SIGPLAN Not. 49, 9 (September 2014), р. 25–38.
DOI: https://doi.org/10.1145/2692915.2628151.

4. Schultz D.A. (2012). Decentralized information flow control for databases (Doctoral dissertation, Massachusetts Institute of Technology). URL: http://hdl.handle.net/1721.1/78363 (дата обращения: 01.02.2023).

5. Guarnieri M., Balliu M., Schoepe D., Basin D. and Sabelfeld A. Information-Flow Control for Database-Backed Applications. IEEE European Symposium on Security and Privacy (EuroS&P), Stockholm, Sweden. 2019, p. 79–94.
DOI: https://10.1109/EuroSP.2019.00016.

6. Kozyri E. et al. Expressing Information Flow Properties. Foundations and Trends® in Privacy and Security. 2022, v. 3, no. 1, p. 1–102. DOI: http://dx.doi.org/10.1561/3300000008.

7. Graf J., Hecker M., Mohr M. & Snelting G. (2015). Checking Applications using Security APIs with JOANA.
URL: https://www.semanticscholar.org/paper/Checking-Applications-using-Security-APIs-with-Graf-Hecker/3ed693338777cb5d4203ff8616efa62ec359673c (дата обращения: 01.02.2023).

8. Andrew C. Myers and Barbara Liskov. 1997. A decentralized model for information flow control. SIGOPS Oper. Syst. Rev. 31, 5 (Dec. 1997), р. 129–142.
DOI: https://doi.org/10.1145/269005.266669.

9. Broberg N., Sands D. (2006). Flow Locks: Towards a Core Calculus for Dynamic Flow Policies. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg.
DOI: https://doi.org/10.1007/11693024_13.

10. Niklas Broberg and David Sands. 2010. Paralocks: role-based information flow control and beyond. SIGPLAN Not. 45, 1 (January 2010), р. 431–444. DOI: https://doi.org/10.1145/1707801.1706349.

11. François Pottier and Vincent Simonet. 2003. Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25, 1 (January 2003), р. 117–158. DOI: https://doi.org/10.1145/596980.596983.

12. Leslie Lamport. 1994. The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 3 (May 1994),
р. 872–923. DOI: https://doi.org/10.1145/177492.177726.

13. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers [Book Review], in Computer, vol. 35, no. 9, p. 81–81, Sept. 2002.
DOI: https://doi.org/10.1109/MC.2002.1033032.

14. Тимаков А.А. Контроль информационных потоков в программных блоках баз данных на основе формальной верификации. Программирование. 2022, № 4, с. 27–49. – EDN: WEMCXC.

15. Niklas Broberg and David Sands. 2009. Flow-sensitive semantics for dynamic information flow policies. In Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS '09). Association for Computing Machinery, New York, NY, USA, р. 101–112.
DOI: https://doi.org/10.1145/1554339.1554352.

16. Moor O. d. et al. Keynote Address: .QL for Source Code Analysis. Seventh IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2007), Paris, France. 2007, p. 3–16.
DOI: https://doi.org/10.1109/SCAM.2007.31.

17. Yu Y., Manolios P., Lamport L. (1999). Model Checking TLA+ Specifications. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science,
vol 1703. Springer, Berlin, Heidelberg.
DOI: https://doi.org/10.1007/3-540-48153-2_6.




DOI: http://dx.doi.org/10.26583/bit.2023.2.03

Ссылки

  • На текущий момент ссылки отсутствуют.


Лицензия Creative Commons
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.