Возможности статической верификации монолитного ядра операционных систем

У большинства современных, повсеместно используемых операционных систем архитектура ядра в той или иной степени является монолитной, поскольку именно данная архитектура позволяет обеспечить максимальную производительность работы. Как правило, размер монолитного ядра без различных расширений, таких как драйверы устройств, составляет несколько миллионов строк кода на языке программирования Си/Си++ и языке ассемблера. С течением времени исходный код достаточно интенсивно изменяется: добавляется поддержка новой функциональности, оптимизируется выполнение различных операций, исправляются ошибки. Высокая практическая значимость монолитного ядра операционных систем определяет строгие требования к его функциональности, безопасности, надежности и производительности. Те подходы к обеспечению качества программных систем, которые в настоящее время используются на практике, позволяют выявить и исправить достаточно большое количество ошибок, однако ни один из них не позволяет обнаружить все возможные ошибки искомых видов. В этой статье показывается, что различные подходы к статической верификации, которые нацелены на решение данной задачи, имеют существенные ограничения, если их применять к монолитному ядру операционных систем целиком, в первую очередь из-за большого размера и сложности исходного кода, который постоянно изменяется. В качестве первого шага в направлении статической верификации монолитного ядра операционных систем предлагается метод декомпозиции ядра на подсистемы.