185 модулей ядра, not‑proved: 0. Сеть и хранилище в Ring 3, TCP работает на железе. Разбор проекта Schild TCB: формальная верификация, изоляция периферии и то, где я упёрся. С честными границами — что доказано, что только в QEMU, а что на реальном ноутбуке. Читать далее
Предлагаю вашему вниманию перевод seL4 Whitepaper, который является хорошим введением в одно из самых известных микроядер для ОС — seL4 (лицензия GPLv2).Здесь не только специфика seL4 и микроядер, но и много полезного материала в целом по безопасности, формальной верификации, виртуализации и системам жёсткого реального времени. Читать далее
Make with Ada – конкурс программных проектов для встраиваемых устройств, спонсируемый компанией AdaCore. В нём могут принять участие независимые разработчики и небольшие группы, использующие языки Ada или SPARK для разработки надежных, открытых и безопасных программ. Цель этого конкурса – распространение информации о преимуществах языков Ada и SPARK и поощрение их использования в новых проектах. Призовой фонд более 8000 €. Читать дальше →
MongoDB объявила о выпуске 10.0 версии коннектора MongoDB для Apache Spark. В этой версии используется новый API Spark Data Sources второй версии (V2) с поддержкой структурированной потоковой передачи данных Spark (Spark Structured Streaming). Зачем нужна новая версия? Текущая версия MongoDB Spark Connector была первоначально…