Новости

07.09.2017: В Падерборне состоялся седьмой Linux Driver Verification Workshop

4-5 сентября 2017 года в Падерборне, Германия состоялся седьмой международный семинар Linux Driver Verification совместно со вторым международным семинаром по инструменту CPAchecker.

28.08.2017: Поиск ошибок, связанных с гонками по данным, в ядре ОС Linux

Антон Волков закончил проект “Поиск ошибок, связанных с гонками по данным, в ядре ОС Linux”, выполненный в рамках Google Summer of Code 2017 под эгидой The Linux Foundation. Целями проекта были:

  1. поиск ошибок, связанных с состояниями гонки, в ядре ОС Linux;
  2. уведомление разработчиков модулей ядра об этих ошибках.

27.08.2017: Поиск ошибок использования памяти в ядре ОС Linux

Антон Васильев закончил проект "Поиск ошибок использования памяти в ядре ОС Linux", выполненный в рамках Google Summer of Code 2017 под эгидой The Linux Foundation. Ошибки использования памяти несут существенные риски для программного обеспечения, но их обнаружение существенно усложняется, если речь идет об операционной системе. Для поиска и отладки таких ошибок в ОС Linux используются специальные сборки ядра ОС.

30.06.2017: В Москве состоялась Международная Ершовская конференция по информатике (PSI-2017)

В Москве прошла 11-я Международная Ершовская конференция по информатике (PSI-2017). В рамках данной конференции Евгений Новиков и Илья Захаров, участвующие в проекте Linux Driver Verification, представили доклад, в котором были затронуты проблемы и особенности применения существующих на сегодняшний день инструментов статической верификации к произвольным программам, разрабатываемым на языке Си с расширениями GNU.

30.05.2017: Компонент AstraVer был представлен на международном семинаре Frama-C & SPARK Day 2017

В презентации на международном семинаре Frama-C & SPARK Day 2017, который состоялся 30 мая в университете Париж Дидро, мы представили наш опыт дедуктивной верификации модулей ядра Linux с помощью платформы Frama-C, Why3 и компонента AstraVer, а также реализованную в нем комбинированную модель ограниченных целых.

27.04.2017: CPAchecker-BAM-BnB и BLAST 2.7.3 на SV-COMP'2017

На международных соревнованиях инструментов статической верификации (SV-COMP 2017), проходящей в рамках международной конференции TACAS, Уппсала, Швеция, были представлены доклады по инструментам CPAchecker-BAM-BnB и BLAST 2.7.3.

30.03.2017: Состоялась конференция «РусКрипто’2017»

XIX научно-практическая конференция «РусКрипто’2017», посвященная различным аспектам криптографии, информационной безопасности и защиты информации прошла 21 — 24 марта 2017 года в подмосковном отеле «Солнечный Park Hotel & SPA».

05.03.2017: 3-4 марта состоялась конференция "Инструменты и методы анализа программ 2017" (TMPA-2017)

В Москве 3-4 марта прошла 4-я международная конференция “Методы и инструменты анализа программ” (TMPA-2017), организованная совместно с ACM Sigsoft. В рамках данной конференции представили доклады Павел Андрианов и Илья Захаров, являющиеся участниками проекта Linux Driver Verification.

30.11.2016: Опубликована новая версия Astraver Toolset 1.1

Инструменты Astraver Toolset 1.1 включают в себя следующие улучшения:

Поддержка языка Си

  • Поддержка адресной арифметики с указателями на вложенные структуры, например, макроса `container_of', широкораспространённого в ядре ОС Linux. В частности, теперь появилась возможность доказать корректность указателя на внешнюю структуру, полученного путём вычитания смещения внутренней структуры из указателя на неё.

Новый подход к целочисленным арифметическим операциям в ACSL

27.09.2016: В Пассау состоялся шестой Linux Driver Verification Workshop

22-23 сентября 2016 года в Пассау, Германия состоялся шестой международный семинар Linux Driver Verification совместно с первым международным семинаром по инструменту CPAchecker.