• Микроядро seL4. Формальная верификация программ в реальном мире

    • Перевод
    Научная статья опубликована в журнале Communications of the ACM, октябрь 2018, том 61, номер 10, стр. 68−77, doi: 10.1145/3230627

    В феврале 2017 года со взлётной площадки «Боинга» в Аризоне поднялся вертолёт с обычным заданием: облёт ближайших холмов. Он летел полностью автономно. Согласно требованиям по технике безопасности Федерального управления авиации США, пилот не прикасался к органам управления. Это был не первый автономный полёт AH-6, которого в компании называют Беспилотной Птичкой (Unmanned Little Bird, ULB). Он так летает уже много лет. Однако на этот раз посреди полёта вертолёт подвергся кибератаке. Бортовой компьютер атаковало вредоносное программное обеспечение видеокамеры, а также вирус, доставленный через заражённую флэшку, которую вставили во время техобслуживания. Атака поставила под угрозу некоторые подсистемы, но не смогла повлиять на безопасную эксплуатацию воздушного судна.
    Читать дальше →
  • Мягкое введение в Coq: структуры данных и функции высших порядков

    • Tutorial

    Пары и списки


    В предыдущих частях мы научились задавать новые типы данных, определять функции над ними и доказывать их корректность с помощью распространенных тактик. Настало время определить некоторые структуры данных и функции высших порядков (далее ФВП) над ними.
    Читать дальше →
  • Мягкое введение в Coq: используем тактики

      Доказательство упрощением


      Итак, в предыдущих частях мы определили новые типы данных и функции над ними. Настало время обратиться к вопросу о том, как сформулировать и доказать их свойства и поведение. В некотором смысле мы уже начали делать это – в первой части мы написали своего рода юнит-тест, используя ключевое слово Example, который содержал некоторые утверждения о поведении некоторой функции, применяемой к определенному набору аргументов. Используя определение функции, Coq упрощает выражение и проверяет на равенство его левую и правую часть.
      Читать дальше →
    • Мягкое введение в Coq: начало

      • Tutorial

      Предисловие


      Ни для кого не секрет, что ошибки в программах могут привести печальным последствиям. История знает множество случаев, когда переполнение счетчика или необработанное исключение приводило к большим материальным затратам и человеческим жертвам. Так, например, 4 июня 1996 года европейская ракета-носитель «Ariane 5» буквально развалилась на части на 39-й секунде полета. Анализ инцидента показал, что авария произошла из-за ошибки в программном обеспечении. Ущерб составил около $7 млрд. В феврале 1991 года ракета «Patriot» промахнулась мимо цели из-за ошибки округления, успела пролететь лишние 500 метров. Ущерб: 28 убитых и более сотни раненых. Подобного рода ошибки встречаются и в аппаратном обеспечении. Недавний баг в процессорах Pentium, связанный с неправильным делением чисел с плавающей точкой, вынудил Intel пойти на замену бракованных чипов. Эта ошибка стоила компании $475 млн.
      Читать дальше →
    • Мягкое введение в Coq: индуктивные определения

      • Tutorial
      В предыдущей части мы научились задавать новые типы и строить функции над их значениями. В этой небольшой заметке я более подробно остановлюсь на индуктивных определениях, чтобы внести ясность и наметить дальнейшие темы для изучения.

      Ранее я сказал, что в Coq нет батареек. На самом деле я слукавил — в Coq есть стандартная библиотека, которая содержит множество полезных определений. Помимо стандартной библиотеки существуют и более специфические вещи, на которых мы пока не будем останавливаться.
      Читать дальше →
      • +10
      • 4,2k
      • 2