Preview

Труды Института системного программирования РАН

Расширенный поиск

Статическая верификация конфигураций ядра Linux

https://doi.org/10.15514/ISPRAS-2017-29(4)-14

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

Аннотация

Ядро операционной системы Linux - это частый пример современных инженерных решений в области создания продуктовых линеек программного обеспечения. Сегодня это одна из наиболее сложных программных систем. Для того, чтобы обеспечить наиболее безопасное построение вариантов продуктовой линейки, необходимо анализировать конфигурационный файл Kconfig помимо исходного кода. Ядро содержит десять тысяч вариабельных переменных несмотря на современную инженерию. Исследователи в области верификации предлагают большое количество решения проблемы анализа. Стандартные процедуры верификации здесь не могут быть применены из-за времени проверки покрытия всех конфигураций. Мы предлагаем инструмент, который базируется на связи уже существующих программах для проверки кода и конфигурационного файла с метрикой покрытия. Такой пакет - это эффективный инструмент для расчета всех допустимых конфигураций для предопределенного набора кода и Kconfig. Предложенные методы могут быть использованы для улучшения существующих инструментов анализа, а также для выбора правильной конфигурации. Наша основная цель - лучше разобраться в возможных дефектах и предложить быстрое и безопасное решение для проверки ядра Linux. Это решение будет описано как программа с инструкцией по реализации внутренней архитектуры.

Об авторах

С. В. Козин
Национальный исследовательский университет Высшая Школа Экономики
Россия


В. С. Мутилин
Институт системного программирования РАН
Россия


Список литературы

1. Jacobson I., Griss M., Jonsson P. Software Reuse, Architecture, Process and Organization for Business Success. Addison-Wesley, 1997.

2. Bosch J. Design and Use of Software Architectures: Adopting and Evolving a Product Line Approach. Pearson Education, 2000.

3. Clements P., Northrop L. Software Product Lines: Practices and Patterns. SEI Series in Software Engineering, Addison-Wesley, 2001.

4. Pohl K., Böckle G., van der Linden F. J. Software Product Line Engineering: Foundations, Principles and Techniques. Springer-Verlag, 2005. DOI: 10.1007/3-540-28901-1.

5. В.В. Кулямин, Е.М. Лаврищева, В.С. Мутилин, А.К. Петренко. “Верификация и анализ вариабельных операционных систем” Труды ИСП РАН, том 28, вып. 3, 2016, стр. 189-208. DOI: 10.15514/ISPRAS-2016-28(3)-12

6. Lotufo R., She S., Berger T., Czarnecki K., Wąsowski A. Evolution of the Linux kernel variability model. Proc. of SPLC’10, LNCS 6287:136-150, Springer, 2010. DOI: 10.1007/978-3-642-15579-6_10.

7. Лаврищева К.М., Коваль Г.И., Слабоспицкая О.O., Колесник А.Л. Особенности процессов управления при создании семейств программных систем. Проблемы программирования, 3:40-49, 2009.

8. Лаврищева К.М., Слабоспицкий А.А., Коваль Г.И., Колесник А.А. Теоретические аспекты управления вариабельностью в семействах программных систем Теоретические аспекты управления вариабельностью в семействах программных систем. Вестник КНУ, серия физ.-мат. наук, 1:151-158, 2011.

9. Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, Dawson Engler, A “Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World”, Communications of the ACM, Vol. 53 No. 2, pp. 66-75

10. Бородин А.Е., Белеванцев А.А., “Статический анализатор Svace как коллекция анализаторов разных уровней сложности” Труды ИСП РАН, том 27, вып. 6, 2015, стр. 111-134. DOI: 10.15514/ISPRAS-2015-27(6)-8

11. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, “The software model checker BLAST”, Int J Softw Tools Technol Transfer (2007) 9:505-525, Springer-Verlag 2007

12. Andy Kenner, Christian Kastner, SteffenHaase, Thomas Leich, “TypeChef: toward type checking #ifdef variability in C”. Proceeding FOSD ’10 Proceedings of the 2nd Internationsal Workchop on Feature-Oriented Software Development, pp. 25-32, Eindhoven, The Netherlands, Oct. 10, 2010.

13. Stephan Henglein. Vampyr configurability aware compile testing of source files. Linux Plumber Conference, Oct 15-17, 2014, Dusseldorf, Germany. Available at: http://www.linuxplumbersconf.net/2014/ocw//system/presentations/2313/original/hengelein.pdf, дата обращения 12.01.2017.

14. Кулямин В., Тестирование на основе моделей. (online publication). http://mbt-course.narod.ru/Lecture03.pdf, дата обращения 12.02.2017.

15. Alber Zever. Pycparcer wiki. (Onine publication). Available at: https://pypi.python.org/pypi/pycparser/2.14. дата обращения 7.05.2017.

16. И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов. Конфигурируемая система статической верификации модулей ядра операционных систем. Труды ИСП РАН, том 26, вып. 2, 2014, стр. 5-42. DOI: 10.15514/ISPRAS-2014-26(2)-1.


Для цитирования:


Козин С.В., Мутилин В.С. Статическая верификация конфигураций ядра Linux. Труды Института системного программирования РАН. 2017;29(4):217-230. https://doi.org/10.15514/ISPRAS-2017-29(4)-14

For citation:


Kozin S.V., Mutilin V.S. Static Verification of Linux Kernel Configurations. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(4):217-230. https://doi.org/10.15514/ISPRAS-2017-29(4)-14

Просмотров: 54


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)