Мне 38 лет, я сварщик из Санкт‑Петербурга. Профильного IT‑образования у меня нет. В июне 2026 года я купил ноутбук, поставил Linux и начал разбираться, как всё устроено изнутри. В октябре с этого же ноутбука я открыл страницу на смартфоне по обычному Wi‑Fi. Страницу отдавала операционная система, которую я собрал сам.
Рубрика «sel4»
Микроядро seL4, Ada-SPARK и 185 модулей: разбор проекта
2026-10-16 в 12:09, admin, рубрики: sel4, spark, TCB, x86_64, микроядро, отладка, формальная верификацияМикроядро seL4. Формальная верификация программ в реальном мире
2019-01-24 в 15:47, admin, рубрики: AH-6, CakeML, CAmkES, Candle, capDL, CertiKOS, CoCon, CompCert, FSCQ, Ivory, Milawa, Rockwell Collins, sel4, ULB, Unmanned Little Bird, Беспилотная Птичка, боинг, гипотеза Кеплера, информационная безопасность, математика, модернизация безопасности ПО, проблема четырёх красок, синтез драйверов, системное программирование, Софт, теорема о нечётном порядке, теорема Фейта — Томпсона, типобезопасность, транспорт будущего, формальная верификацияНаучная статья опубликована в журнале Communications of the ACM, октябрь 2018, том 61, номер 10, стр. 68−77, doi: 10.1145/3230627
В феврале 2017 года со взлётной площадки «Боинга» в Аризоне поднялся вертолёт с обычным заданием: облёт ближайших холмов. Он летел полностью автономно. Согласно требованиям по технике безопасности Федерального управления авиации США, пилот не прикасался к органам управления. Это был не первый автономный полёт AH-6, которого в компании называют Беспилотной Птичкой (Unmanned Little Bird, ULB). Он так летает уже много лет. Однако на этот раз посреди полёта вертолёт подвергся кибератаке. Бортовой компьютер атаковало вредоносное программное обеспечение видеокамеры, а также вирус, доставленный через заражённую флэшку, которую вставили во время техобслуживания. Атака поставила под угрозу некоторые подсистемы, но не смогла повлиять на безопасную эксплуатацию воздушного судна.
Читать полностью »