DIFFuzzer: шаг на пути к тестированию файловых систем на основе спецификаций

В статье описан следующий шаг развития мутационного дифференциального фаззера файловых систем DIFFuzzer, предполагающий интеграцию формальных спецификаций для улучшения его возможностей тестирования. Изначально DIFFuzzer разрабатывался на основе дифференциального подхода с интеграцией в исходный код модели POSIX, что ограничивало гибкость и масштабируемость инструмента. Предлагаемый улучшенный подход разделяет логику фаззера и модель при помощи выделения последней во внешнюю формальную спецификацию, написанную на языке LibSL. Это позволяет создавать более точные тестовые оракулы и облегчает генерацию рабочей нагрузки. В данной работе мы подробно описываем текущее состояние проекта, включая расширение LibSL и реализацию тестового оракула на основе спецификаций. Также описаны направления будущей работы и связанные с ними проблемы, такие как совершенствование формальной спецификации POSIX и развитие модуля генерации рабочей нагрузки на основе спецификаций.

1. Ковалевский В.М., Кечин В.В., Ицыксон В.М. DIFFuzzer: обнаружение ошибок файловых систем с помощью дифференциального фаззинга серого ящика. Труды ИСП РАН, 2025, том 37, вып. 4, часть 2, стр. 31-46 (на английском языке). DOI: 10.15514/ISPRAS–2025–37(4)–17. / Kovalevsky V.M., Kechin V.V., Itsykson V.M. DIFFuzzer: Detecting File System Errors with Differential Grey-box Fuzzing. Trudy ISP RAN/Proc. ISP RAS, 2025, vol. 37, issue 4 (part 2), pp. 31-46. DOI: 10.15514/ISPRAS-2025-37(4)-17.

2. Ковалевский В.М., Кечин В.В., Янин А.С., Ицыксон В.М. Легковесная проверка согласованности файловой системы после сбоев с помощью дифференциального фаззинга. Труды ИСП РАН, 2026, том 38, вып. 1, стр. 79-92 (на английском языке). DOI: 10.15514/ISPRAS–2026–38(1)–7. / Kovalevsky V. M., Kechin V. V., Yanin A. S., Itsykson V. M. Lightweight file system crash-consistency checking with differential fuzzing. Trudy ISP RAN/Proc. ISP RAS, 2026, vol. 38, issue 1, pp. 79-92. DOI: 10.15514/ISPRAS-2026-38(1)-7.

3. Miller B.P., Fredriksen L., So B. An empirical study of the reliability of UNIX utilities. Commun. ACM, 1990, vol. 33, no. 12, pp. 32–44. DOI: 10.1145/96267.96279.

4. Manes V.J. M., Han H., Han C., Cha S.K., Egele M., Schwartz E.J., Woo M. The Art, Science, and Engineering of Fuzzing: A Survey. IEEE Transactions on Software Engineering, 2021, vol. 47, no. 11, pp. 2312–2331. DOI: 10.1109/TSE.2019.2946563.

5. IEEE/Open Group standard for information technology–portable operating system interface (POSIX™) base specifications, issue 8. IEEE/Open Group Std 1003.1-2024 (Revision of IEEE Std 1003.1-2017), 2024, 4107 p.

6. Itsykson V.M. Partial Specifications of Libraries: Applications in Software Engineering. Communications in Computer and Information Science, 2021, vol. 1288, pp. 3-25. DOI: 10.1007/978-3-030-71472-7_1.

7. Itsykson V.M. LibSL: Language for Specification of Software Libraries. PROGRAMMNAYA INGENERIA, 2018, vol. 9, pp. 209-220. DOI: 10.17587/prin.9.209-220.

8. Bourdonov I.B., Kossatchev A.S., Kuliamin V.V., Petrenko A.K. UniTesK Test Suite Architecture, 2002, pp. 77-88. DOI: 10.1007/3-540-45614-7_5.

9. Гриневич А.И., Кулямин В.В., Марковцев Д.А., Петренко А.К., Рубанов В.В., Хорошилов А.В. Использование формальных методов для обеспечения соблюдения программных стандартов. Труды ИСП РАН, 2006, том 10. / Grinevich A.I., Kulyamin V.V., Markovtsev D.A., Petrenko A.K., Rubanov V.V., Khoroshilov A.V. Using formal methods to ensure compliance with software standards. Trudy ISP RAN/Proc. ISP RAS, 2006, vol. 27 (in Russian).

10. Groce A., Holzmann G., Joshi R. Randomized Differential Testing as a Prelude to Formal Verification, 2007, pp. 621-631. DOI: 10.1109/ICSE.2007.68.

11. McKeeman W.M. Differential Testing for Software. Digit. Tech. J, 1998, vol. 10, pp. 100-107.

12. Petrenko A. Model-based testing. In Proceedings of the 27th international conference on Software engineering (ICSE '05). Association for Computing Machinery, 2005, pp. 722-723. DOI: 10.1145/1062455.1062636.

13. Xu M. et al. Krace: Data race fuzzing for kernel file systems. IEEE Symposium on Security and Privacy (SP). IEEE, 2020, pp. 1643-1660. DOI: 10.1109/SP40000.2020.00078.

14. Clements A.T. et al. The scalable commutativity rule: Designing scalable software for multicore processors. ACM Transactions on Computer Systems (TOCS). Association for Computing Machinery, 2015, vol. 32. issue 4, pp. 1-47. DOI: 10.1145/2699681.

15. Fuchs N. Specifications are (preferably) executable. Software Engineering Journal, 1992, pp. 323-334.

16. Lamport L. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Boston, MA, United States, 2002, 364 p.

17. Jackson D. Software Abstractions - Logic, Language, and Analysis. The MIT Press, Cambridge, MA, United States, 2006.

18. Liu Y. et al. Metis: File system model checking via versatile input and state exploration. 22nd USENIX Conference on File and Storage Technologies (FAST 24). USENIX Association, 2024, pp. 123-140.

19. Ridge T. et al. SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. Proceedings of the 25th Symposium on Operating Systems Principles. Association for Computing Machinery, 2015, pp. 38-53. DOI: 10.1145/2815400.2815411.

20. Bornholt J. et al. Specifying and checking file system crash-consistency models. Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems. Association for Computing Machinery, 2016, pp. 83-98. DOI: 10.1145/2872362.2872406.

21. Torlak E., Bodik R. Growing solver-aided languages with rosette. Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software. Association for Computing Machinery, 2013, pp. 135-152. DOI: 10.1145/2509578.2509586.