The seL4 microkernel. Formal verification of programs in the real world
Scientific article published in the journal Communications of the ACM , October 2018, Volume 61, Number 10, pp. 68–77, doi: 10.1145 / 3230627
In February 2017, a helicopter took off from the Boeing takeoff site in Arizona with the usual mission: circling the nearest hills. He flew completely autonomously. According to the safety requirements of the US Federal Aviation Administration, the pilot did not touch the controls. It was not the first autonomous flight of the AH-6, which the company calls the Unmanned Little Bird (ULB). He has been flying for many years. However, this time in the middle of the flight, the helicopter was subjected to a cyber attack. The on-board computer attacked the malicious software of the camcorder, as well as a virus, delivered through an infected flash drive, which was inserted during maintenance. The attack threatened some subsystems, but could not affect the safe operation of the aircraft.
You might think that military aircraft will easily reflect such a cyber attack. In reality, a team of professional pentesters commissioned by DARPA as part of a program to develop highly reliable military computer systems High-Assurance Cyber Military Systems (HACMS) in 2013 successfully cracked the first version of the ULB software, which was originally designed to ensure flight safety, not from cyber attacks. Hackers were able to break the helicopter or put it on any place at will. Therefore, the risk of such attacks with a passenger on board is difficult to overestimate, and an unsuccessful hacking attempt in February 2017 indicates some fundamental changes in software.
This article explains these changes and the technology that made them possible. This is a technology developed in the framework of the HACMS program aimed at ensuring the safe operation of critical systems in a hostile cyber environment - in this case, several autonomous vehicles. The technology is based on formal software verification — these are programs with automatically verified mathematical proofs that work according to their specification. Although the article is not devoted to the formal methods themselves, it explains how to use artifact verification to protect real systems in practice.
Perhaps the most impressive result of HACMS is that the technology can be extended to existing real systems, significantly improving their protection against cyber attacks. This process is called "seismic security retrofit" (seismic security retrofit) by analogy with seismic retrofit of buildings. Moreover, most of the reengineering is done by Boeing engineers, not by formal verification specialists.
"Birdie" during an unmanned test flight
Not all software on a helicopter is built on mathematical models and proofs. The field of formal verification is not yet ready for such a scale. However, the HACMS program has demonstrated that the strategic application of formal methods to the most important parts of the overall system significantly improves security. The HACMS approach works for systems in which the desired security property can be achieved through purely enforced application at the architecture level. It is based on our verified sel4 microkernel, which we will discuss below. It guarantees isolation between subsystems, with the exception of clearly defined communication channels that are subject to system security policies. This isolation is guaranteed at the architecture level using the CAmkES verified framework for system components. Using domain-specific languages from Galois Inc. The CAmkES platform integrates with architecture analysis tools from Rockwell Collins and the University of Minnesota, as well as highly reliable software components.
HACMS achievements are based on the old faithful friend of the software engineer - modularization. The innovation is that formal methods prove the observability of interfaces and the encapsulation of module internals. This guaranteed adherence to modularity allows engineers who are not experts in formal methods (like at Boeing) to create new or even modernize existing systems and achieve high stability. Although the tools do not yet provide complete proof of system security.
Evidence of the mathematical correctness of programs dates back to at least the 1960s , but for a long time their real value for software development was limited to scale and depth. However, in recent years, there have been a number of impressive breakthroughs in formal verification at the code level of real systems, from the verified C CompCert compiler to the verified seL4 microkernel (see scientific articles about it), the verified CoCon conference system, the verified ML CakeML compiler, verified programs for proving theorems by Milawa and Candle , a verified file system with FSCQ crash protection , a verified IronFleet distributed system and a verified CertiKOS parallel kernel framework , as well as important m mathematical theorems, including four-color problems , automatic proof of Kepler's conjecture, and Feit-Thompson theorem on odd order . These are all real systems. For example, CompCert is a commercial product, the seL4 microkernel is used in aerospace and unmanned aircraft as a platform for the Internet of Things, and CoCon has been used at numerous major scientific conferences.
These verification projects require considerable effort. To make formal methods publicly available, these efforts need to be reduced. Here we demonstrate how a strategic combination of formal and informal methods, partial automation of formal methods and careful software development to maximize the benefits of isolated components allowed us to significantly increase the reliability of systems, the total size and complexity of which are orders of magnitude larger than those mentioned above.
Please note that we apply formal verification primarily for the code on which the security of the system depends. But there are other benefits. For example, proof of correctness of the code makes assumptions about the context in which it runs (for example, hardware behavior and software configuration). Formal verification makes these assumptions explicit, which helps developers focus on other means of verification, such as testing. In addition, in many cases, the system includes both verified and unverified code. During code review, testing and debugging, formal verification acts like a lens, focusing on the critical untested system code.
Let's start with the foundation for building provably reliable systems - the operating system kernel (OS). This is the most important part, which guarantees the reliability of the entire system cost-effectively.
The seL4 microkernel provides a formally verified minimum set of mechanisms for implementing secure systems. Unlike standard kernels , it is purposefully universal and therefore suitable for implementing a number of security policies and system requirements.
One of the main goals of seL4 development is to provide strong isolation between mutually distrustful components that run on top of the kernel. It is supported as a hypervisor, for example, for entire Linux operating systems, while keeping them isolated from security-critical components that can work together, as shown in Figure 1. In particular, this feature allows system developers to use obsolete components with hidden vulnerabilities next to highly reliable components.
Fig. 1. Isolation and controlled communications in seL4
The seL4 core occupies a special position among general-purpose microkernels. Not only does it provide better performance in its class , its 10,000 lines of C code underwent a more thorough formal verification than any other open source software in the history of mankind in terms of not only proof lines, but also durability of proven properties. The basis is the proof of the "functional correctness" of the implementation of the kernel in C. It ensures that any behavior of the kernel is predicted by its formal abstract specification: see the online application for an overview of what this evidence looks like. Following this guarantee, we have added additional evidence that will be explained after the introduction of the basic mechanisms of the kernel.
The seL4 core provides a minimal set of mechanisms for implementing secure systems: threads, ability management, virtual address spaces, interprocess communication (IPC), signaling, and interrupt delivery.
The kernel maintains its state in “kernel objects”. For example, for each flow in the system, there is a “flow object” that stores information about scheduling, execution, and access control. User-space programs can only refer to kernel objects indirectly through so-called “capabilities” or “capabilities” (capabilities), which combine a link to an object with a set of access rights to it. For example, a thread cannot start or stop another thread if it does not have the “ability” for the corresponding stream object.
Threads interact and synchronize by sending messages through end-point (endpoint) objects of the interprocess communication. One thread with the ability to send to the appropriate endpoint can send a message to another thread that has the ability to receive to that endpoint. Notification objects (notification) provide synchronization through sets of binary semaphores. Virtual address translation is controlled by kernel objects that represent page directories, page tables, and frame objects or subtle abstractions over the corresponding processor architecture objects. Each stream has a specific ability “VSpace”, which points to the root of the object tree for address translation of the stream. The capabilities themselves are controlled by the kernel and are stored in the “CNodes” kernel objects located in the structure of the graph that maps references to objects with access rights, similar to the comparison of virtual page tables with physical addresses in memory. Each thread has its own CNode root identification ability. The set of abilities available from this root is called the “CSpace Stream.” Abilities can be transferred through the endpoints with the transfer of work, and they can also be declared common using shared CSpace. Figure 2 shows these kernel objects.
Fig. 2. Kernel objects in the system on seL4 with two threads interacting through the end point
Due to its versatility, the seL4 kernel APIs operate at a low level and support highly dynamic system architectures. Therefore, direct evidence for these APIs is problematic to obtain.
The high-level concept of access control policies abstracts from individual objects and kernel capabilities, instead capturing the system's access control configuration using a set of abstract "subjects" (components) and powers that each of them has over others (for example, to read data and send messages) . In the example in fig. 2, components A and B have authority over the end point.
Sewell and his colleagues proved that seL4 access control policies ensure that two basic security features are observed: restriction of authority and integrity.
Restriction of authority means that the access control policy is a static (immutable) safe approximation of specific capabilities and kernel objects in the system for any future state. This property implies that no matter how the system evolves, no component will ever get more authority than the access control policy predicts. In Figure 2, the policy for component B does not contain write access to component A. Thus, component B can never get this access in the future. This property implies that policy-based reasoning is a safe approximation to the reasoning about a particular access control state in the system.
Integrity means that no matter what the component does, it can never change the data in the system (including any system calls it can make) that it does not explicitly allow it to change the access control policy. For example, in fig. 2, the only component of authority A over another component is the right to send data to the end point, from which component B receives information. This means that component A can only change its state, the state of stream B, and the state of the message buffer. It cannot change other parts of the system.
A side effect of integrity is confidentiality, when a component is unable to read information from another component without permission : it is a proven strong property of the non-transitive non-interference of seL4. That is, in a properly configured system (with more stringent restrictions than just for integrity), none of the components will be able to find out information about another component or its execution without permission. Proof expresses this property in terms of an information flow policy that can be extracted from the access control policy used in the proof of integrity. Information will be transmitted only when explicitly permitted by the policy. The proof covers explicit information flows as well as potential channels of hidden storage in the kernel. But synchronization channels are outside its scope and must be processed by other means .
Further evidence in seL4 includes the extension of functional correctness and, therefore, safety theorems to the binary level for the ARMv7 architecture and the worst runtime profile for the kernel ( 1 , 2 ) required for real-time systems. The seL4 core is available for different architectures: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 and Intel x64. At the moment, it has passed a machine test on the ARMv7 architecture for the entire verification stack, as well as on ARMv7a with hypervisor extensions for functional correctness.
The previous section describes the software methods by which the seL4 core creates a solid foundation for provably reliable systems. The kernel forms a reliable computing base (TCB) - a mandatory component of the software, which is required to work correctly for guaranteed system security. In real systems, this base is much broader than just a microkernel. It is necessary to verify an additional software stack in order to gain the same level of confidence as for the kernel. However, there are classes of systems for which there is no need for such verification: they need only isolation theorems at the kernel level to derive certain security properties at the system level. This section provides an example of such a system.
These are systems in which the component architectures have already implemented a critical property, possibly along with several small trusted components. Our example is the flight control software of a quadrocopter, a demonstration device in the HACMS program mentioned earlier.
Figure 3 shows the main hardware components of the quadrocopter. The architecture is intentionally more complex than that required for a quadrocopter, since it was supposed to represent ULB and at this level of abstraction is similar to the ULB architecture.
Fig. 3. Autonomous aircraft architecture
The figure shows two main computers: an on-board computer that interacts with the ground station and controls the on-board software (for example, a camera), and a navigation computer for controlling the flight of the vehicle, reading sensor data and controlling the engines. Computers are connected via an internal network or CAN bus on a quadcopter, Ethernet on ULB. The quadcopter also has an unprotected WiFi point, which makes it possible to demonstrate additional methods of protection.
In this example, consider the on-board computer. For it must be four basic properties:
The working hypothesis is that the camera is unreliable, potentially compromised or harmful, that its drivers and outdated software are potentially compromised, just like any external communication channels. In this example, we assume correct and strong cryptography, that is, that the key cannot be picked up, and we deduce the possibility of the enemy's suppression of radio communication with a ground station beyond the scope of the task.
Figure 4 shows how the quadcopter architecture is designed, which provides these properties. A Linux virtual machine (VM) serves as a container for outdated software for onboard devices, camera drivers and WiFi points. We isolate the cryptographic control module in our own component, with connections to the CAN bus, the ground station channel and the Linux virtual machine to send data to the ground station. The task of the cryptographic component is to transfer (only) authorized messages to the on-board computer via the stack CAN interface and send diagnostic data back to the ground station. The radio component sends and receives unprocessed messages that are encrypted and decrypted (authenticated) by the cryptographic component.
Fig.4. Simplified quadcopter board computer architecture
The installation of the desired properties of the system is reduced solely to the properties of isolation and the behavior of the architecture in terms of information flows, as well as to the behavior of a single trusted cryptographic component. Assuming the correct behavior of this component, the keys cannot be compromised, since no other component has access to them. The channel between Linux and the cryptographic component in fig. 4 is intended only for the transfer of messages and does not give access to memory. Only authorized messages can get onto the CAN bus, because the cryptographic component is the only connection to the bus. Unreliable software and WiFi, as part of a Linux virtual machine, are encapsulated by component isolation and can only interact with the rest of the system through a trusted cryptographic component.
It is easy to imagine that this kind of architecture analysis can be largely automated by checking models and tools of higher-level mechanical reasoning. As noted for MILS systems , the boundaries of components in such an architecture are not only a convenient tool for moduleing and code management, but with forced isolation provide effective boundaries for formal reasoning about the system behavior. However, it all depends on the correct use of the component boundaries at run time in the final binary implementation of the system.
The seL4 core mechanisms discussed earlier are capable of providing such an implementation, but the level of abstraction of the mechanisms contrasts sharply with the blocks and arrows of the architectural scheme: an even more abstract access control policy still contains much more details than the architecture diagram. In a real system of this size, there are tens of thousands of kernel objects and “abilities” created by software, and configuration errors can lead to security breaches. Then we will discuss how we not only automate the configuration and creation of such code, but also how to automatically prove compliance with the boundaries of the architecture.
As security evidence is simplified with formal abstractions of security policies, abstraction also helps in system design. The Camkes component platform runs on seL4 abstractions over low-level kernel mechanisms, providing communication primitives and system decomposition into functional units, as shown in Figure. 5. Using this platform, system architects can design and build systems based on seL4 in terms of high-level components that interact with each other and with hardware devices via connectors, such as remote procedure call (RPC), dataports and events.
Fig. 5. Workflow CAmkES
Internally, CAmkES implements these abstractions using low-level seL4 core objects. Each component contains (at least) one stream, CSpace and VSpace. RPC connectors use endpoint objects, and CAmkES generates intermediate code to process messages and transfer them over IPC endpoints. Similarly, a dataport connector is implemented through shared memory — common frames present in the address spaces of the two components — and optionally can limit the direction of data transfer. Finally, the event connector is implemented using the seL4 notification mechanism.
CAmkES also generates in capDL a low-level specification of the initial configuration of objects and the capabilities of the system kernel. Эта спецификация становится входными данными для инициализатора seL4, который первым запускается после загрузки и выполняет необходимые операции seL4 для создания инстанса и инициализации системы .
Таким образом, платформа компонентов генерирует код без дополнительных усилий со стороны разработчика. Компонентная архитектура описывает набор блоков и стрелок, а задача реализации сводится к простому заполнению полей. Платформа генерирует остальное, обеспечивая реализацию описанной архитектуры.
На платформе с традиционными компонентами сгенерированный код расширит доверенную вычислительную базу системы, поскольку он может влиять на функциональность компонентов. Однако CAmkES также генерирует доказательства.
При генерации «промежуточного» кода CAmkES производит формальные доказательства в Isabelle/HOL, выполняя валидацию в процессе трансляции и демонстрируя, что сгенерированный «промежуточный» код подчиняется спецификации высокого уровня, а сгенерированная спецификация capDL является правильным уточнением описания CAmkES . Мы также доказали, что инициализатор seL4 правильно настраивает систему в требуемой начальной конфигурации. При этом мы автоматизируем большую часть построения системы без расширения доверенной вычислительной базы.
Разработчики редко смотрят на выдачу генераторов кода, их интересует только функциональность и бизнес-логика. Так же и мы предполагаем, что доказательства для промежуточного кода не нуждаются в проверке, то есть разработчики могут сосредоточиться на доказательстве корректности собственного кода. Как сгенерированный CAmkES заголовок даёт разработчику API для сгенерированного кода, так и операторы леммы верхнего уровня производят API для доказательств. Леммы описывают ожидаемое поведение коннекторов. В примере промежуточного кода RPC на рис. 6 сгенерированная функция f предоставляет способ вызова удалённой функции g в другом компоненте. Чтобы сохранить абстракции, вызов f должен быть эквивалентен вызову g . Сгенерированная системой лемма гарантирует, что f из сгенерированного кода RPC ведёт себя как прямой вызов g .
Fig. 6. Cгенерированный код RPC
Для реального использования сгенерированных системой доказательств они должны быть компонуемы с (почти) произвольными доказательствами, предоставленными пользователем, как для функции g , так и для контекстов, в которых используются g and f . Чтобы добиться этой компонуемости, спецификация коннекторов параметризуется через предоставленные пользователем спецификации удалённых функций. Таким образом, инженеры могут рассуждать о своей архитектуре, предоставляя спецификации и доказательства для своих компонентов, и полагаться на спецификации для сгенерированного кода.
На сегодняшний день мы продемонстрировали этот процесс от начала и до конца с помощью специального коннектора CAmkES RPC ( 1 , 2 ). Поскольку шаблоны других коннекторов (датапорты и события) значительно проще, чем RPC, будет несложно расширить генератор доказательств для поддержки этих коннекторов, что позволит создавать более разнообразные верифицированные системы.
После кода для коммуникации CAmkES создаёт начальную конфигурацию управления доступом для применения границ архитектуры. Чтобы доказать, что эти два описания системы — capDL и CAmkES — соответствуют друг другу, рассмотрим описание CAmkES как абстракцию для описание capDL. Используем упомянутый ранее проверенный фреймворк , чтобы вывести полномочия одного объекта над другим объектом из описания capDL. Так мы повысим доказательство до уровня политики. Кроме того, мы определили правила для вывода полномочий между компонентами в описании CAmkES. Полученное доказательство гарантирует, что у объектов capDL, представленных в виде графа полномочий с объектами, сгруппированными по компонентам, те же границы между группами, что и в эквивалентном графе компонентов CAmkES . Интуитивно, такое соответствие границ означает, что анализ архитектуры политики из описания CAmkES сохранит политику из описания, сгенерированного capDL, которое, в свою очередь, гарантированно удовлетворяет требованиям ограничения полномочий, целостности и конфиденциальности, как упоминалось ранее.
Наконец, для доказательства корректной инициализации CAmkES использует универсальный инициализатор, который запустится как первая пользовательская задача после загрузки. В seL4 эта первая (и уникальная) пользовательская задача имеет доступ ко всей доступной памяти, используя её для создания объектов и «способностей» в соответствии с подробным описанием capDL, которое она принимает в качестве входных данных. Доказано, что состояние после выполнения инициализатора удовлетворяет состоянию, описанному в заданной спецификации . Это доказательство справедливо для точной модели инициализатора, но ещё не на уровне реализации. По сравнению с глубиной остальной цепи доказательств это ограничение может показаться слабым, но оно уже является более формальным доказательством, чем требуется на высшем уровне (EAL7) общих критериев оценки безопасности.
На практике трудно обеспечить разработку системы с нуля ради безопасности, поэтому решающее значение для разработки безопасных систем имеет возможность модернизации старого ПО. Наш фреймворк на базе seL4 поддерживает итеративный процесс, который мы называем «сейсмическая модернизация безопасности», как обычный архитектор модернизирует существующие здания для большей сейсмоустойчивости. Проиллюстрируем процесс на примере постепенной адаптации существующей программной архитектуры беспилотного вертолёта, перейдя от традиционного схемы тестирования к высоконадёжной системе с теоремами, подкреплёнными формальными методами. Хотя этот пример основан на реальном проекте ULB, здесь он упрощён и не включает все детали.
Оригинальная архитектура вертолёта совпадает с архитектурой, описанной на рис. 3. Его функциональность обеспечивают два отдельных компьютера: навигационный вычислитель управляет фактическим полётом, а бортовой компьютер выполняет задачи высокого уровня (такие как связь с наземной станцией и навигация по картинке с камеры). Первоначальная версия бортового компьютера была монолитным приложением под Linux. В процессе модернизации инженеры компании «Боинг» применили методы, инструменты и компоненты, предоставленные партнёрами по программе HACMS.
Первым шагом было принять систему как есть и запустить ее в виртуальной машине поверх безопасного гипервизора (см. рис. 7). В метафоре сейсмической модернизации это соответствует размещению системы на более подвижном фундаменте. Виртуальная машина поверх seL4 в этой системе состоит из одного компонента CAmkES, который включает монитор виртуальной машины (VMM) и гостевую операционную систему, в данном случае Linux. Ядро предоставляет абстракции оборудования виртуализации, а VMM управляет этими абстракциями для виртуальной машины. Ядро seL4 ограничивает не только гостевую ОС, но и VMM, поэтому не нужно доверять реализации VMM для обеспечения принудительной изоляции. Отказ VMM приведёт к отказу гостевой ОС, но не к отказу всей системы.
Fig. 7. Все функциональные возможности в одной виртуальной машине
В зависимости от конфигурации системы, виртуальная машина может иметь доступ к устройствам через паравиртуализированные драйверы, сквозные драйверы или обоими способами. В случае сквозных драйверов разработчики могут использовать системный MMU или IOMMU для предотвращения нарушения границ изоляции аппаратными устройствами и драйверами в гостевой системе. Обратите внимание, что простой запуск системы на виртуальной машине не добавляет дополнительных преимуществ безопасности или надёжности. Шаг 1 нужен только для подготовки к шагу 2.
Второй шаг сейсмической модернизации усиливает существующие стены. В программном обеспечении разработчик может повысить безопасность и надёжность, разделив исходную систему на несколько подсистем, каждая из которых состоит из виртуальной машины, выполняющей код только части исходной системы. Каждая комбинация VM/VMM выполняется в отдельном компоненте CAmkES, который внедряет изоляцию между разными подсистемами, не позволяя им влиять друг на друга, а затем допускает сожительство разных уровней безопасности.
В целом, разделы следуют существующей архитектуре ПО, хотя если архитектуры недостаточно для эффективной изоляции, может потребоваться перепроектирование.
Как правило, разделы должны взаимодействовать друг с другом, так что на этом этапе мы также добавим каналы связи. Для обеспечения безопасности крайне важно, чтобы эти интерфейсы были узкими, ограничивая связь между разделами только тем, что абсолютно необходимо. Кроме того, интерфейсные протоколы должны быть эффективными, с минимальным количеством сообщений или объёмом данных. Критически важно, что seL4 позволяет контролировать и ограничивать обмен памятью между разделами, чтобы минимизировать объём данных.
Помимо виртуальных машин, представляющих подсистемы исходной системы, мы также извлекаем и реализуем компоненты для любых общих ресурсов (таких как сетевой интерфейс).
Можно повторять шаг 2 до тех пор, пока мы не достигнем желаемой детализации разделов. Правильная детализация — это компромисс между прочностью изоляции, с одной стороны, и повышенными накладными расходами на коммуникации и затратами на реконструкцию, с другой стороны.
В нашем примере мы получили три раздела: виртуальную машину, реализующую функции связи наземной станции под управлением Linux; другую виртуальную машину, реализующую функции навигации на основе камеры (также работающую под управлением Linux); и нативный компонент, предоставляющий общий доступ к сети, как показано на рис. eight.
Рис.8. Функциональность разделена на несколько виртуальных машин
Когда система разложена на отдельные разделы виртуальной машины, некоторые или все отдельные разделы можно повторно реализовать в виде нативных компонентов, а не виртуальных машин. Это значительно уменьшит поверхность атаки для той же функциональности. Дополнительное преимущество преобразования компонента в машинный код — снижение нагрузки и повышение производительности, удаление гостевой ОС и накладных расходов на исполнение кода и коммуникации VMM.
Нативные компоненты также повышают потенциал применения формальной верификации и других методов для повышения надёжности компонента. Варианты разные: от полной функциональной проверки собственного кода до совместной генерации кода и доказательств, проверки модели, использования типобезопасных языков программирования, статического анализа или традиционного тщательного тестирования меньшей кодовой базы.
Благодаря изоляции, которую обеспечивают seL4 и компонентная архитектура, становится возможной совместная работа в системе компонентов с разными уровнями надёжности. В этом случае компоненты низкой надёжности не уменьшают общую надёжность системы, а разработчики выигрывают от того, что не нужно тратить усилия на верификацию этого кода.
В нашем примере разберём на нативные модули виртуальную машину для канала связи между бортовым компьютером и наземной станцией. В нативных компонентах реализуются функции связи, криптографии и управления (mission-manager). Мы оставим в виртуальной машине камеру и WiFi как ненадёжный устаревший компонент (см. рис. 9). Такое разделение стало компромиссом между усилиями по переделке подсистем и выгодами от использования нативных компонентов с точки зрения производительности и надёжности.
Fig. 9. Функциональность реализована в нативных компонентах
Получив все необходимые модули, сделаем заключительный шаг: анализ всей системы в целом на основе надёжности архитектуры и отдельных компонентов.
В рамках HACMS коммуникация, криптография, и модуль управления реализованы на доказуемо типобезопасном предметно-ориентированном языке Ivory , с выделением фиксированного объёма памяти в куче. Без дополнительной верификации Ivory не даёт нам гарантий функциональной корректности, но даёт уверенность в отказоустойчивости и аварийной надёжности. Учитывая изоляцию компонентов, мы считаем, что эти гарантии сохраняются в присутствии ненадёжных компонентов (таких как виртуальная машина камеры).
Сетевой компонент реализован на стандартном коде C, состоящем из пользовательского кода для платформы и уже существующего кода библиотеки. Его уровень надёжности соответствует уровню, полученному благодаря тщательной реализации известного кода. Надёжность можно повысить без особых затрат с помощью таких методов, как синтез драйверов , а также с помощью типобезопасных языков вроде Ivory. В общем анализе безопасности системы любая компрометация сетевого компонента повлияет только на сетевые пакеты. Поскольку трафик зашифрован, такая атака не поставит под угрозу условие из спецификаций, что в бортовой компьютер попадают только авторизованные команды.
Виртуальная машина видеокамеры — самая слабая часть системы, так как она работает в системе Linux и в ней предполагается наличие уязвимостей. Но VM изолирована, так что если злоумышленники её взломают, они не смогут перейти к другим компонентам. Самое худшее, что может сделать злоумышленник, — это отправить неверные данные компоненту управления. Как и в квадрокоптере, этот компонент проверяет данные, полученные от камеры. И он успешно выдержал кибератаку, упомянутую в начале статьи. Это была атака типа «белый ящик», где команде пентестеров дали доступ ко всему коду и документации, а также ко всем внешним каналам коммуникаций. Ей намеренно предоставили рутовый доступ к виртуальной машине камеры, имитируя успешную атаку на устаревшее программное обеспечение. Сдерживание атаки и способность защититься от этого очень мощного сценария стали достойной проверкой наших требований безопасности и выявления любых пропущенных предположений, проблем интерфейса или других проблем безопасности, которые исследовательская группа могла не распознать.
В этой статье приведён обзор метода достижения очень высоких уровней безопасности для систем, в которых свойство безопасности применимо через компонентную архитектуру. Мы доказали теоремы для уровня ядра и его правильной конфигурации, а также теоремы, которые гарантируют, что компонентная платформа правильно настраивает границы защиты в соответствии с описанием своей архитектуры, и что она генерирует правильный код для удалённых вызовов процедур. Связь с высокоуровневым анализом безопасности системы остаётся неформальной, а теоремы коммуникационного кода не покрывают все примитивы коммуникаций, предоставленные платформой. Для автоматического получения теоремы, которая покрывает всю систему от начала до конца, требуется проделать дополнительную работу. Однако на данном этапе ясно, что это осуществимая задача.
Основная цель представленной работы заключается в резком сокращении усилий по проверке для конкретных классов систем. Описанный здесь чисто архитектурный подход можно расширить на другие системы, кроме ULB, но он явно ограничен тем фактом, что может выражать только свойства, которые определяются компонентной архитектурой системы. Отдача уменьшится, если эта архитектура изменяется во время выполнения программы, а также если свойства критически зависят от поведения слишком большого числа доверенных компонентов или компонентов слишком большого размера.
Первый шаг к ослаблению этих ограничений — создание библиотеки предварительно проверенных компонентов высокого уровня надёжности для использования в качестве надёжных строительных блоков в таких архитектурах. Эта библиотека может включать шаблоны безопасности (такие как дезинфекция входных данных, фильтры вывода, мониторы снижения уровня секретности и времени выполнения), потенциально сгенерированные из спецификаций более высокого уровня, а также такие компоненты инфраструктуры, как повторно используемые криптомодули, хранилище ключей, файловые системы, сетевые стеки и драйверы высокой надёжности. Если безопасность зависит более чем от одного такого компонента, то возникает необходимость обосновать надёжность их взаимодействия и совместного использования. Основными техническими проблемами здесь являются рассуждения о параллелизме и протоколах, а также о потоке информации в присутствии доверенных компонентов. Несмотря на эти ограничения, работа демонстрирует быстрое развитие реальных высоконадёжных систем на основе seL4. В настоящее время создание таких систем возможно за меньшую стоимость, чем традиционное тестирование.
Разработка дизайна и кода seL4 заняла два человеко-года. Если добавить все серотип-специфичные доказательства, в общей сложности получится 18 человеко-лет для 8700 строк кода на C. Для сравнения, разработка сравнимого по размеру микроядра L4Ka::Pistachio из семейства seL4 заняло шесть человеко-лет и не обеспечило значительного уровня надёжности. Это означает разницу по скорости разработки всего лишь в 3,3 раза между верифицированным и традиционным софтом. Согласно методу оценки Кольбера и Бома , сертификация по традиционным критериям EAL7 для 8700 строк кода C займёт более 45,9 человеко-лет. Это означает, что формальная верификация реализации на бинарном уровне уже в 2,3 раза дешевле, чем самый высокий уровень сертификации по общим критериям, при этом обеспечивает значительно более высокую надёжность.
Для сравнения, описанный здесь подход HACMS использует для каждой новой системы только существующие доказательства, включая доказательства, сгенерированные инструментами. Таким образом, общие усилия по доказательству для системы, которая соответствует этому подходу, сводятся к человеко-неделям, а не годам, а тестирование сводится только к проверке допущений.
In February 2017, a helicopter took off from the Boeing takeoff site in Arizona with the usual mission: circling the nearest hills. He flew completely autonomously. According to the safety requirements of the US Federal Aviation Administration, the pilot did not touch the controls. It was not the first autonomous flight of the AH-6, which the company calls the Unmanned Little Bird (ULB). He has been flying for many years. However, this time in the middle of the flight, the helicopter was subjected to a cyber attack. The on-board computer attacked the malicious software of the camcorder, as well as a virus, delivered through an infected flash drive, which was inserted during maintenance. The attack threatened some subsystems, but could not affect the safe operation of the aircraft.Key ideas
- Formal proofs from the software architecture of a verified microkernel can be inexpensively scaled to real systems.
- Different levels of security and reliability within the same system are possible and desirable. It is not necessary to ensure maximum reliability of the entire code.
- Reasonably moderate redesign and refactoring to raise existing systems to the level of highly reliable code.
You might think that military aircraft will easily reflect such a cyber attack. In reality, a team of professional pentesters commissioned by DARPA as part of a program to develop highly reliable military computer systems High-Assurance Cyber Military Systems (HACMS) in 2013 successfully cracked the first version of the ULB software, which was originally designed to ensure flight safety, not from cyber attacks. Hackers were able to break the helicopter or put it on any place at will. Therefore, the risk of such attacks with a passenger on board is difficult to overestimate, and an unsuccessful hacking attempt in February 2017 indicates some fundamental changes in software.
This article explains these changes and the technology that made them possible. This is a technology developed in the framework of the HACMS program aimed at ensuring the safe operation of critical systems in a hostile cyber environment - in this case, several autonomous vehicles. The technology is based on formal software verification — these are programs with automatically verified mathematical proofs that work according to their specification. Although the article is not devoted to the formal methods themselves, it explains how to use artifact verification to protect real systems in practice.
Perhaps the most impressive result of HACMS is that the technology can be extended to existing real systems, significantly improving their protection against cyber attacks. This process is called "seismic security retrofit" (seismic security retrofit) by analogy with seismic retrofit of buildings. Moreover, most of the reengineering is done by Boeing engineers, not by formal verification specialists.
"Birdie" during an unmanned test flight
Not all software on a helicopter is built on mathematical models and proofs. The field of formal verification is not yet ready for such a scale. However, the HACMS program has demonstrated that the strategic application of formal methods to the most important parts of the overall system significantly improves security. The HACMS approach works for systems in which the desired security property can be achieved through purely enforced application at the architecture level. It is based on our verified sel4 microkernel, which we will discuss below. It guarantees isolation between subsystems, with the exception of clearly defined communication channels that are subject to system security policies. This isolation is guaranteed at the architecture level using the CAmkES verified framework for system components. Using domain-specific languages from Galois Inc. The CAmkES platform integrates with architecture analysis tools from Rockwell Collins and the University of Minnesota, as well as highly reliable software components.
HACMS achievements are based on the old faithful friend of the software engineer - modularization. The innovation is that formal methods prove the observability of interfaces and the encapsulation of module internals. This guaranteed adherence to modularity allows engineers who are not experts in formal methods (like at Boeing) to create new or even modernize existing systems and achieve high stability. Although the tools do not yet provide complete proof of system security.
Formal verification
Evidence of the mathematical correctness of programs dates back to at least the 1960s , but for a long time their real value for software development was limited to scale and depth. However, in recent years, there have been a number of impressive breakthroughs in formal verification at the code level of real systems, from the verified C CompCert compiler to the verified seL4 microkernel (see scientific articles about it), the verified CoCon conference system, the verified ML CakeML compiler, verified programs for proving theorems by Milawa and Candle , a verified file system with FSCQ crash protection , a verified IronFleet distributed system and a verified CertiKOS parallel kernel framework , as well as important m mathematical theorems, including four-color problems , automatic proof of Kepler's conjecture, and Feit-Thompson theorem on odd order . These are all real systems. For example, CompCert is a commercial product, the seL4 microkernel is used in aerospace and unmanned aircraft as a platform for the Internet of Things, and CoCon has been used at numerous major scientific conferences.
These verification projects require considerable effort. To make formal methods publicly available, these efforts need to be reduced. Here we demonstrate how a strategic combination of formal and informal methods, partial automation of formal methods and careful software development to maximize the benefits of isolated components allowed us to significantly increase the reliability of systems, the total size and complexity of which are orders of magnitude larger than those mentioned above.
Please note that we apply formal verification primarily for the code on which the security of the system depends. But there are other benefits. For example, proof of correctness of the code makes assumptions about the context in which it runs (for example, hardware behavior and software configuration). Formal verification makes these assumptions explicit, which helps developers focus on other means of verification, such as testing. In addition, in many cases, the system includes both verified and unverified code. During code review, testing and debugging, formal verification acts like a lens, focusing on the critical untested system code.
seL4
Let's start with the foundation for building provably reliable systems - the operating system kernel (OS). This is the most important part, which guarantees the reliability of the entire system cost-effectively.
The seL4 microkernel provides a formally verified minimum set of mechanisms for implementing secure systems. Unlike standard kernels , it is purposefully universal and therefore suitable for implementing a number of security policies and system requirements.
One of the main goals of seL4 development is to provide strong isolation between mutually distrustful components that run on top of the kernel. It is supported as a hypervisor, for example, for entire Linux operating systems, while keeping them isolated from security-critical components that can work together, as shown in Figure 1. In particular, this feature allows system developers to use obsolete components with hidden vulnerabilities next to highly reliable components.
Fig. 1. Isolation and controlled communications in seL4
The seL4 core occupies a special position among general-purpose microkernels. Not only does it provide better performance in its class , its 10,000 lines of C code underwent a more thorough formal verification than any other open source software in the history of mankind in terms of not only proof lines, but also durability of proven properties. The basis is the proof of the "functional correctness" of the implementation of the kernel in C. It ensures that any behavior of the kernel is predicted by its formal abstract specification: see the online application for an overview of what this evidence looks like. Following this guarantee, we have added additional evidence that will be explained after the introduction of the basic mechanisms of the kernel.
seL4 API
The seL4 core provides a minimal set of mechanisms for implementing secure systems: threads, ability management, virtual address spaces, interprocess communication (IPC), signaling, and interrupt delivery.
The kernel maintains its state in “kernel objects”. For example, for each flow in the system, there is a “flow object” that stores information about scheduling, execution, and access control. User-space programs can only refer to kernel objects indirectly through so-called “capabilities” or “capabilities” (capabilities), which combine a link to an object with a set of access rights to it. For example, a thread cannot start or stop another thread if it does not have the “ability” for the corresponding stream object.
Threads interact and synchronize by sending messages through end-point (endpoint) objects of the interprocess communication. One thread with the ability to send to the appropriate endpoint can send a message to another thread that has the ability to receive to that endpoint. Notification objects (notification) provide synchronization through sets of binary semaphores. Virtual address translation is controlled by kernel objects that represent page directories, page tables, and frame objects or subtle abstractions over the corresponding processor architecture objects. Each stream has a specific ability “VSpace”, which points to the root of the object tree for address translation of the stream. The capabilities themselves are controlled by the kernel and are stored in the “CNodes” kernel objects located in the structure of the graph that maps references to objects with access rights, similar to the comparison of virtual page tables with physical addresses in memory. Each thread has its own CNode root identification ability. The set of abilities available from this root is called the “CSpace Stream.” Abilities can be transferred through the endpoints with the transfer of work, and they can also be declared common using shared CSpace. Figure 2 shows these kernel objects.
Fig. 2. Kernel objects in the system on seL4 with two threads interacting through the end point
Evidence of safety
Due to its versatility, the seL4 kernel APIs operate at a low level and support highly dynamic system architectures. Therefore, direct evidence for these APIs is problematic to obtain.
The high-level concept of access control policies abstracts from individual objects and kernel capabilities, instead capturing the system's access control configuration using a set of abstract "subjects" (components) and powers that each of them has over others (for example, to read data and send messages) . In the example in fig. 2, components A and B have authority over the end point.
Sewell and his colleagues proved that seL4 access control policies ensure that two basic security features are observed: restriction of authority and integrity.
Restriction of authority means that the access control policy is a static (immutable) safe approximation of specific capabilities and kernel objects in the system for any future state. This property implies that no matter how the system evolves, no component will ever get more authority than the access control policy predicts. In Figure 2, the policy for component B does not contain write access to component A. Thus, component B can never get this access in the future. This property implies that policy-based reasoning is a safe approximation to the reasoning about a particular access control state in the system.
Integrity means that no matter what the component does, it can never change the data in the system (including any system calls it can make) that it does not explicitly allow it to change the access control policy. For example, in fig. 2, the only component of authority A over another component is the right to send data to the end point, from which component B receives information. This means that component A can only change its state, the state of stream B, and the state of the message buffer. It cannot change other parts of the system.
A side effect of integrity is confidentiality, when a component is unable to read information from another component without permission : it is a proven strong property of the non-transitive non-interference of seL4. That is, in a properly configured system (with more stringent restrictions than just for integrity), none of the components will be able to find out information about another component or its execution without permission. Proof expresses this property in terms of an information flow policy that can be extracted from the access control policy used in the proof of integrity. Information will be transmitted only when explicitly permitted by the policy. The proof covers explicit information flows as well as potential channels of hidden storage in the kernel. But synchronization channels are outside its scope and must be processed by other means .
Further evidence in seL4 includes the extension of functional correctness and, therefore, safety theorems to the binary level for the ARMv7 architecture and the worst runtime profile for the kernel ( 1 , 2 ) required for real-time systems. The seL4 core is available for different architectures: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 and Intel x64. At the moment, it has passed a machine test on the ARMv7 architecture for the entire verification stack, as well as on ARMv7a with hypervisor extensions for functional correctness.
Security Architecture
The previous section describes the software methods by which the seL4 core creates a solid foundation for provably reliable systems. The kernel forms a reliable computing base (TCB) - a mandatory component of the software, which is required to work correctly for guaranteed system security. In real systems, this base is much broader than just a microkernel. It is necessary to verify an additional software stack in order to gain the same level of confidence as for the kernel. However, there are classes of systems for which there is no need for such verification: they need only isolation theorems at the kernel level to derive certain security properties at the system level. This section provides an example of such a system.
These are systems in which the component architectures have already implemented a critical property, possibly along with several small trusted components. Our example is the flight control software of a quadrocopter, a demonstration device in the HACMS program mentioned earlier.
Figure 3 shows the main hardware components of the quadrocopter. The architecture is intentionally more complex than that required for a quadrocopter, since it was supposed to represent ULB and at this level of abstraction is similar to the ULB architecture.
Fig. 3. Autonomous aircraft architecture
The figure shows two main computers: an on-board computer that interacts with the ground station and controls the on-board software (for example, a camera), and a navigation computer for controlling the flight of the vehicle, reading sensor data and controlling the engines. Computers are connected via an internal network or CAN bus on a quadcopter, Ethernet on ULB. The quadcopter also has an unprotected WiFi point, which makes it possible to demonstrate additional methods of protection.
In this example, consider the on-board computer. For it must be four basic properties:
- correct authentication of commands from the ground station;
- cryptographic keys privacy;
- no additional messages for the navigation calculator;
- unreliable software from other onboard systems can not affect the flight of the device.
The working hypothesis is that the camera is unreliable, potentially compromised or harmful, that its drivers and outdated software are potentially compromised, just like any external communication channels. In this example, we assume correct and strong cryptography, that is, that the key cannot be picked up, and we deduce the possibility of the enemy's suppression of radio communication with a ground station beyond the scope of the task.
Figure 4 shows how the quadcopter architecture is designed, which provides these properties. A Linux virtual machine (VM) serves as a container for outdated software for onboard devices, camera drivers and WiFi points. We isolate the cryptographic control module in our own component, with connections to the CAN bus, the ground station channel and the Linux virtual machine to send data to the ground station. The task of the cryptographic component is to transfer (only) authorized messages to the on-board computer via the stack CAN interface and send diagnostic data back to the ground station. The radio component sends and receives unprocessed messages that are encrypted and decrypted (authenticated) by the cryptographic component.
Fig.4. Simplified quadcopter board computer architecture
The installation of the desired properties of the system is reduced solely to the properties of isolation and the behavior of the architecture in terms of information flows, as well as to the behavior of a single trusted cryptographic component. Assuming the correct behavior of this component, the keys cannot be compromised, since no other component has access to them. The channel between Linux and the cryptographic component in fig. 4 is intended only for the transfer of messages and does not give access to memory. Only authorized messages can get onto the CAN bus, because the cryptographic component is the only connection to the bus. Unreliable software and WiFi, as part of a Linux virtual machine, are encapsulated by component isolation and can only interact with the rest of the system through a trusted cryptographic component.
It is easy to imagine that this kind of architecture analysis can be largely automated by checking models and tools of higher-level mechanical reasoning. As noted for MILS systems , the boundaries of components in such an architecture are not only a convenient tool for moduleing and code management, but with forced isolation provide effective boundaries for formal reasoning about the system behavior. However, it all depends on the correct use of the component boundaries at run time in the final binary implementation of the system.
The seL4 core mechanisms discussed earlier are capable of providing such an implementation, but the level of abstraction of the mechanisms contrasts sharply with the blocks and arrows of the architectural scheme: an even more abstract access control policy still contains much more details than the architecture diagram. In a real system of this size, there are tens of thousands of kernel objects and “abilities” created by software, and configuration errors can lead to security breaches. Then we will discuss how we not only automate the configuration and creation of such code, but also how to automatically prove compliance with the boundaries of the architecture.
Component Representation Verification
As security evidence is simplified with formal abstractions of security policies, abstraction also helps in system design. The Camkes component platform runs on seL4 abstractions over low-level kernel mechanisms, providing communication primitives and system decomposition into functional units, as shown in Figure. 5. Using this platform, system architects can design and build systems based on seL4 in terms of high-level components that interact with each other and with hardware devices via connectors, such as remote procedure call (RPC), dataports and events.
Fig. 5. Workflow CAmkES
Code generation
Internally, CAmkES implements these abstractions using low-level seL4 core objects. Each component contains (at least) one stream, CSpace and VSpace. RPC connectors use endpoint objects, and CAmkES generates intermediate code to process messages and transfer them over IPC endpoints. Similarly, a dataport connector is implemented through shared memory — common frames present in the address spaces of the two components — and optionally can limit the direction of data transfer. Finally, the event connector is implemented using the seL4 notification mechanism.
CAmkES also generates in capDL a low-level specification of the initial configuration of objects and the capabilities of the system kernel. Эта спецификация становится входными данными для инициализатора seL4, который первым запускается после загрузки и выполняет необходимые операции seL4 для создания инстанса и инициализации системы .
Таким образом, платформа компонентов генерирует код без дополнительных усилий со стороны разработчика. Компонентная архитектура описывает набор блоков и стрелок, а задача реализации сводится к простому заполнению полей. Платформа генерирует остальное, обеспечивая реализацию описанной архитектуры.
На платформе с традиционными компонентами сгенерированный код расширит доверенную вычислительную базу системы, поскольку он может влиять на функциональность компонентов. Однако CAmkES также генерирует доказательства.
Автоматические доказательства
При генерации «промежуточного» кода CAmkES производит формальные доказательства в Isabelle/HOL, выполняя валидацию в процессе трансляции и демонстрируя, что сгенерированный «промежуточный» код подчиняется спецификации высокого уровня, а сгенерированная спецификация capDL является правильным уточнением описания CAmkES . Мы также доказали, что инициализатор seL4 правильно настраивает систему в требуемой начальной конфигурации. При этом мы автоматизируем большую часть построения системы без расширения доверенной вычислительной базы.
Разработчики редко смотрят на выдачу генераторов кода, их интересует только функциональность и бизнес-логика. Так же и мы предполагаем, что доказательства для промежуточного кода не нуждаются в проверке, то есть разработчики могут сосредоточиться на доказательстве корректности собственного кода. Как сгенерированный CAmkES заголовок даёт разработчику API для сгенерированного кода, так и операторы леммы верхнего уровня производят API для доказательств. Леммы описывают ожидаемое поведение коннекторов. В примере промежуточного кода RPC на рис. 6 сгенерированная функция f предоставляет способ вызова удалённой функции g в другом компоненте. Чтобы сохранить абстракции, вызов f должен быть эквивалентен вызову g . Сгенерированная системой лемма гарантирует, что f из сгенерированного кода RPC ведёт себя как прямой вызов g .
Fig. 6. Cгенерированный код RPC
Для реального использования сгенерированных системой доказательств они должны быть компонуемы с (почти) произвольными доказательствами, предоставленными пользователем, как для функции g , так и для контекстов, в которых используются g and f . Чтобы добиться этой компонуемости, спецификация коннекторов параметризуется через предоставленные пользователем спецификации удалённых функций. Таким образом, инженеры могут рассуждать о своей архитектуре, предоставляя спецификации и доказательства для своих компонентов, и полагаться на спецификации для сгенерированного кода.
На сегодняшний день мы продемонстрировали этот процесс от начала и до конца с помощью специального коннектора CAmkES RPC ( 1 , 2 ). Поскольку шаблоны других коннекторов (датапорты и события) значительно проще, чем RPC, будет несложно расширить генератор доказательств для поддержки этих коннекторов, что позволит создавать более разнообразные верифицированные системы.
После кода для коммуникации CAmkES создаёт начальную конфигурацию управления доступом для применения границ архитектуры. Чтобы доказать, что эти два описания системы — capDL и CAmkES — соответствуют друг другу, рассмотрим описание CAmkES как абстракцию для описание capDL. Используем упомянутый ранее проверенный фреймворк , чтобы вывести полномочия одного объекта над другим объектом из описания capDL. Так мы повысим доказательство до уровня политики. Кроме того, мы определили правила для вывода полномочий между компонентами в описании CAmkES. Полученное доказательство гарантирует, что у объектов capDL, представленных в виде графа полномочий с объектами, сгруппированными по компонентам, те же границы между группами, что и в эквивалентном графе компонентов CAmkES . Интуитивно, такое соответствие границ означает, что анализ архитектуры политики из описания CAmkES сохранит политику из описания, сгенерированного capDL, которое, в свою очередь, гарантированно удовлетворяет требованиям ограничения полномочий, целостности и конфиденциальности, как упоминалось ранее.
Наконец, для доказательства корректной инициализации CAmkES использует универсальный инициализатор, который запустится как первая пользовательская задача после загрузки. В seL4 эта первая (и уникальная) пользовательская задача имеет доступ ко всей доступной памяти, используя её для создания объектов и «способностей» в соответствии с подробным описанием capDL, которое она принимает в качестве входных данных. Доказано, что состояние после выполнения инициализатора удовлетворяет состоянию, описанному в заданной спецификации . Это доказательство справедливо для точной модели инициализатора, но ещё не на уровне реализации. По сравнению с глубиной остальной цепи доказательств это ограничение может показаться слабым, но оно уже является более формальным доказательством, чем требуется на высшем уровне (EAL7) общих критериев оценки безопасности.
Сейсмическая модернизация безопасности
На практике трудно обеспечить разработку системы с нуля ради безопасности, поэтому решающее значение для разработки безопасных систем имеет возможность модернизации старого ПО. Наш фреймворк на базе seL4 поддерживает итеративный процесс, который мы называем «сейсмическая модернизация безопасности», как обычный архитектор модернизирует существующие здания для большей сейсмоустойчивости. Проиллюстрируем процесс на примере постепенной адаптации существующей программной архитектуры беспилотного вертолёта, перейдя от традиционного схемы тестирования к высоконадёжной системе с теоремами, подкреплёнными формальными методами. Хотя этот пример основан на реальном проекте ULB, здесь он упрощён и не включает все детали.
Оригинальная архитектура вертолёта совпадает с архитектурой, описанной на рис. 3. Его функциональность обеспечивают два отдельных компьютера: навигационный вычислитель управляет фактическим полётом, а бортовой компьютер выполняет задачи высокого уровня (такие как связь с наземной станцией и навигация по картинке с камеры). Первоначальная версия бортового компьютера была монолитным приложением под Linux. В процессе модернизации инженеры компании «Боинг» применили методы, инструменты и компоненты, предоставленные партнёрами по программе HACMS.
Шаг 1. Виртуализация
Первым шагом было принять систему как есть и запустить ее в виртуальной машине поверх безопасного гипервизора (см. рис. 7). В метафоре сейсмической модернизации это соответствует размещению системы на более подвижном фундаменте. Виртуальная машина поверх seL4 в этой системе состоит из одного компонента CAmkES, который включает монитор виртуальной машины (VMM) и гостевую операционную систему, в данном случае Linux. Ядро предоставляет абстракции оборудования виртуализации, а VMM управляет этими абстракциями для виртуальной машины. Ядро seL4 ограничивает не только гостевую ОС, но и VMM, поэтому не нужно доверять реализации VMM для обеспечения принудительной изоляции. Отказ VMM приведёт к отказу гостевой ОС, но не к отказу всей системы.
Fig. 7. Все функциональные возможности в одной виртуальной машине
В зависимости от конфигурации системы, виртуальная машина может иметь доступ к устройствам через паравиртуализированные драйверы, сквозные драйверы или обоими способами. В случае сквозных драйверов разработчики могут использовать системный MMU или IOMMU для предотвращения нарушения границ изоляции аппаратными устройствами и драйверами в гостевой системе. Обратите внимание, что простой запуск системы на виртуальной машине не добавляет дополнительных преимуществ безопасности или надёжности. Шаг 1 нужен только для подготовки к шагу 2.
Шаг 2. Несколько виртуальных машин
Второй шаг сейсмической модернизации усиливает существующие стены. В программном обеспечении разработчик может повысить безопасность и надёжность, разделив исходную систему на несколько подсистем, каждая из которых состоит из виртуальной машины, выполняющей код только части исходной системы. Каждая комбинация VM/VMM выполняется в отдельном компоненте CAmkES, который внедряет изоляцию между разными подсистемами, не позволяя им влиять друг на друга, а затем допускает сожительство разных уровней безопасности.
В целом, разделы следуют существующей архитектуре ПО, хотя если архитектуры недостаточно для эффективной изоляции, может потребоваться перепроектирование.
Как правило, разделы должны взаимодействовать друг с другом, так что на этом этапе мы также добавим каналы связи. Для обеспечения безопасности крайне важно, чтобы эти интерфейсы были узкими, ограничивая связь между разделами только тем, что абсолютно необходимо. Кроме того, интерфейсные протоколы должны быть эффективными, с минимальным количеством сообщений или объёмом данных. Критически важно, что seL4 позволяет контролировать и ограничивать обмен памятью между разделами, чтобы минимизировать объём данных.
Помимо виртуальных машин, представляющих подсистемы исходной системы, мы также извлекаем и реализуем компоненты для любых общих ресурсов (таких как сетевой интерфейс).
Можно повторять шаг 2 до тех пор, пока мы не достигнем желаемой детализации разделов. Правильная детализация — это компромисс между прочностью изоляции, с одной стороны, и повышенными накладными расходами на коммуникации и затратами на реконструкцию, с другой стороны.
В нашем примере мы получили три раздела: виртуальную машину, реализующую функции связи наземной станции под управлением Linux; другую виртуальную машину, реализующую функции навигации на основе камеры (также работающую под управлением Linux); и нативный компонент, предоставляющий общий доступ к сети, как показано на рис. eight.
Рис.8. Функциональность разделена на несколько виртуальных машин
Шаг 3. Нативные компоненты
Когда система разложена на отдельные разделы виртуальной машины, некоторые или все отдельные разделы можно повторно реализовать в виде нативных компонентов, а не виртуальных машин. Это значительно уменьшит поверхность атаки для той же функциональности. Дополнительное преимущество преобразования компонента в машинный код — снижение нагрузки и повышение производительности, удаление гостевой ОС и накладных расходов на исполнение кода и коммуникации VMM.
Нативные компоненты также повышают потенциал применения формальной верификации и других методов для повышения надёжности компонента. Варианты разные: от полной функциональной проверки собственного кода до совместной генерации кода и доказательств, проверки модели, использования типобезопасных языков программирования, статического анализа или традиционного тщательного тестирования меньшей кодовой базы.
Благодаря изоляции, которую обеспечивают seL4 и компонентная архитектура, становится возможной совместная работа в системе компонентов с разными уровнями надёжности. В этом случае компоненты низкой надёжности не уменьшают общую надёжность системы, а разработчики выигрывают от того, что не нужно тратить усилия на верификацию этого кода.
В нашем примере разберём на нативные модули виртуальную машину для канала связи между бортовым компьютером и наземной станцией. В нативных компонентах реализуются функции связи, криптографии и управления (mission-manager). Мы оставим в виртуальной машине камеру и WiFi как ненадёжный устаревший компонент (см. рис. 9). Такое разделение стало компромиссом между усилиями по переделке подсистем и выгодами от использования нативных компонентов с точки зрения производительности и надёжности.
Fig. 9. Функциональность реализована в нативных компонентах
Шаг 4. Надёжность системы в целом
Получив все необходимые модули, сделаем заключительный шаг: анализ всей системы в целом на основе надёжности архитектуры и отдельных компонентов.
В рамках HACMS коммуникация, криптография, и модуль управления реализованы на доказуемо типобезопасном предметно-ориентированном языке Ivory , с выделением фиксированного объёма памяти в куче. Без дополнительной верификации Ivory не даёт нам гарантий функциональной корректности, но даёт уверенность в отказоустойчивости и аварийной надёжности. Учитывая изоляцию компонентов, мы считаем, что эти гарантии сохраняются в присутствии ненадёжных компонентов (таких как виртуальная машина камеры).
Сетевой компонент реализован на стандартном коде C, состоящем из пользовательского кода для платформы и уже существующего кода библиотеки. Его уровень надёжности соответствует уровню, полученному благодаря тщательной реализации известного кода. Надёжность можно повысить без особых затрат с помощью таких методов, как синтез драйверов , а также с помощью типобезопасных языков вроде Ivory. В общем анализе безопасности системы любая компрометация сетевого компонента повлияет только на сетевые пакеты. Поскольку трафик зашифрован, такая атака не поставит под угрозу условие из спецификаций, что в бортовой компьютер попадают только авторизованные команды.
Виртуальная машина видеокамеры — самая слабая часть системы, так как она работает в системе Linux и в ней предполагается наличие уязвимостей. Но VM изолирована, так что если злоумышленники её взломают, они не смогут перейти к другим компонентам. Самое худшее, что может сделать злоумышленник, — это отправить неверные данные компоненту управления. Как и в квадрокоптере, этот компонент проверяет данные, полученные от камеры. И он успешно выдержал кибератаку, упомянутую в начале статьи. Это была атака типа «белый ящик», где команде пентестеров дали доступ ко всему коду и документации, а также ко всем внешним каналам коммуникаций. Ей намеренно предоставили рутовый доступ к виртуальной машине камеры, имитируя успешную атаку на устаревшее программное обеспечение. Сдерживание атаки и способность защититься от этого очень мощного сценария стали достойной проверкой наших требований безопасности и выявления любых пропущенных предположений, проблем интерфейса или других проблем безопасности, которые исследовательская группа могла не распознать.
Ограничения и будущая работа
В этой статье приведён обзор метода достижения очень высоких уровней безопасности для систем, в которых свойство безопасности применимо через компонентную архитектуру. Мы доказали теоремы для уровня ядра и его правильной конфигурации, а также теоремы, которые гарантируют, что компонентная платформа правильно настраивает границы защиты в соответствии с описанием своей архитектуры, и что она генерирует правильный код для удалённых вызовов процедур. Связь с высокоуровневым анализом безопасности системы остаётся неформальной, а теоремы коммуникационного кода не покрывают все примитивы коммуникаций, предоставленные платформой. Для автоматического получения теоремы, которая покрывает всю систему от начала до конца, требуется проделать дополнительную работу. Однако на данном этапе ясно, что это осуществимая задача.
Основная цель представленной работы заключается в резком сокращении усилий по проверке для конкретных классов систем. Описанный здесь чисто архитектурный подход можно расширить на другие системы, кроме ULB, но он явно ограничен тем фактом, что может выражать только свойства, которые определяются компонентной архитектурой системы. Отдача уменьшится, если эта архитектура изменяется во время выполнения программы, а также если свойства критически зависят от поведения слишком большого числа доверенных компонентов или компонентов слишком большого размера.
Первый шаг к ослаблению этих ограничений — создание библиотеки предварительно проверенных компонентов высокого уровня надёжности для использования в качестве надёжных строительных блоков в таких архитектурах. Эта библиотека может включать шаблоны безопасности (такие как дезинфекция входных данных, фильтры вывода, мониторы снижения уровня секретности и времени выполнения), потенциально сгенерированные из спецификаций более высокого уровня, а также такие компоненты инфраструктуры, как повторно используемые криптомодули, хранилище ключей, файловые системы, сетевые стеки и драйверы высокой надёжности. Если безопасность зависит более чем от одного такого компонента, то возникает необходимость обосновать надёжность их взаимодействия и совместного использования. Основными техническими проблемами здесь являются рассуждения о параллелизме и протоколах, а также о потоке информации в присутствии доверенных компонентов. Несмотря на эти ограничения, работа демонстрирует быстрое развитие реальных высоконадёжных систем на основе seL4. В настоящее время создание таких систем возможно за меньшую стоимость, чем традиционное тестирование.
Приложение: трудозатраты
Разработка дизайна и кода seL4 заняла два человеко-года. Если добавить все серотип-специфичные доказательства, в общей сложности получится 18 человеко-лет для 8700 строк кода на C. Для сравнения, разработка сравнимого по размеру микроядра L4Ka::Pistachio из семейства seL4 заняло шесть человеко-лет и не обеспечило значительного уровня надёжности. Это означает разницу по скорости разработки всего лишь в 3,3 раза между верифицированным и традиционным софтом. Согласно методу оценки Кольбера и Бома , сертификация по традиционным критериям EAL7 для 8700 строк кода C займёт более 45,9 человеко-лет. Это означает, что формальная верификация реализации на бинарном уровне уже в 2,3 раза дешевле, чем самый высокий уровень сертификации по общим критериям, при этом обеспечивает значительно более высокую надёжность.
Для сравнения, описанный здесь подход HACMS использует для каждой новой системы только существующие доказательства, включая доказательства, сгенерированные инструментами. Таким образом, общие усилия по доказательству для системы, которая соответствует этому подходу, сводятся к человеко-неделям, а не годам, а тестирование сводится только к проверке допущений.
Source: https://habr.com/ru/post/437406/