Публикации сентябрьского номера журнала Computer посвящены использованию формальных методов при проектировании киберфизических систем: обсуждается эволюция таких методов, и публикуются работы, посвященные устранению пробелов в этой области.
Компьютерные системы сегодня интегрированы не только во всевозможные устройства, но и в различные социальные инфраструктуры, однако на данный момент остро не хватает методов конструирования киберфизических систем с гарантиями их корректного поведения в нормальных и аномальных условиях — отсутствуют даже принципы определения такого поведения. Применение формальных методов при разработке киберфизических систем сдерживается из-за того, что существующие методологии и инструменты попросту не подходят для формализации корректного поведения таких систем.
Сентябрьский номер открывает статья «Интерпретируемая диагностика отказов киберфизических систем: метод на основе обучения» (Interpretable Fault Diagnosis for Cyberphysical Systems: A Learning Perspective), которую подготовили Цзыцюань Дэн (Ziquan Deng) и Чжаодань Кун (Zhaodan Kong). Авторы предлагают применять темпоральную логику сигналов (Signal Temporal Logic, STL) для представления аномалий в показаниях датчиков, полученных путем обучения. Системы диагностики отказов на основе непрерывного обучения предложено моделировать в виде временных автоматов. Отмечено, что формулы STL позволяют выражать надежность как меру минимального или максимального выхода значения сигнала за пределы ожидаемых границ в течение некоторого промежутка времени. Предложен механизм указания характеристик окружающей среды, когда система проверки модели находит ветви, не являющиеся закрытыми и не ведущие к контрпримерам из-за неверных данных об окружающей среде.
Мейи Ма (Meiyi Ma), Джон Станкович (John Stankovic) и Лу Фэн (Lu Feng) опубликовали статью «Формальные методы для умных городов» (Toward Formal Methods for Smart Cities), посвященную трудностям формального моделирования соответствующих систем. Обсуждаются вопросы формальной спецификации, эксплуатационного мониторинга и обучения. По мнению авторов, возможностей STL недостаточно для мониторинга состояния всех городских систем, прогнозирования их состояний в будущем и обеспечения гарантий того, что результаты глубинного обучения будут удовлетворять требованиям города. Для исправления ситуации исследователи предлагают темпоральную логику сигналов с пространственной агрегацией (SaSTL) — расширение STL операторами пространственной агрегации и счетчиками. Описывается инструмент эксплуатационного мониторинга выполнения требований умного города, заданных с помощью SaSTL. Обсуждается возможность улучшения пригодности городов для жизни благодаря такому инструменту.
Умный город оснащен множеством датчиков, системами машинного обучения и искусственного интеллекта, которые запоминают и регулируют параметры умных зданий и энергосетей, динамически обеспечивая комфортные условия проживания, экономию энергии, транспортировку по запросу и т. д. В статье сформулированы задачи обучения умного города, описан инструмент мониторинга для обучающихся систем.
Гуаняо Чэнь (Guangyao Chen) и Чжихао Цзян (Zhihao Jiang) подготовили статью «Моделирование среды в ходе проверки модели киберфизических систем» (Environment Modeling During Model Checking of Cyberphysical Systems), в которой обсуждаются проблемы моделирования сред и проверки модели требований к киберфизическим системам. Авторы предлагают независимую от области применения схему абстрагирования модели среды с возможностью предоставления интерпретируемых контрпримеров, обеспечивающую необходимый охват видов поведения среды; киберфизические системы и среды при этом моделируются с использованием временных автоматов. Описывается методика замкнутого цикла создания системы проверки модели киберфизических систем. Чтобы обеспечить как можно более полный охват возможных нарушений требований, в схеме используют узел с контрпримерами, дочерние узлы которого их не имеют. Как считают авторы, это позволяет задавать больше подробностей в базовой модели и дереве абстракции.
Статья «Практический пример формального моделирования безопасного и защищенного автоматизированного производства» (A Case Study in the Formal Modeling of Safe and Secure Manufacturing Automation), которую опубликовали Мэтью Яблонски (Matthew Jablonski), Бо Ю (Bo Yu), Габриэла Чокарли (Gabriela Ciocarlie) и Пауло Кост (Paulo Cost), описывает формальную спецификацию системы производства алюминиевых банок. Для создания сценариев процесса изготовления банок используется темпоральная логика, а для указания архитектурных элементов, их возможных отказов и атак применяется язык Architecture Analysis and Design Language (AADL). Публикация стала первой попыткой использования AADL при анализе производительности распределенной жестко синхронизированной АСУТП с целью определения того, насколько такая АСУТП удовлетворяет системным ограничениям и спецификациям. Как поясняется, описываемое жестко синхронизированное распределенное производство состоит из множества заводов, которые работают синхронно, чтобы каждый из них мог соблюдать сроки, имея соответствующие механизмы отработки на отказ. Каждый такой завод — это многоуровневая система, в которой конструкция верхних уровней зависит от того, насколько нижние уровни способны удовлетворять требованиям к отработке отказа, предоставлять соответствующие сведения смежным заводам и операторам для минимизации потерь энергии и материалов и своевременно выпускать требуемую продукцию.
Октябрьский номер Computer освещает проблему объяснимости искусственного интеллекта и машинного обучения. Применений таких систем сегодня масса — от обнаружения финансового мошенничества до марсианских миссий. Системы внедряются повсеместно, но можно ли им доверять и полагаться на решения, принимаемые машиной? Важным процессом, который позволяет укрепить доверие к этим непрозрачным системам и повысить их надежность, является анализ процедуры принятия решений для получения объяснения соответствующих механизмов. Это многогранная задача, ведь нужно еще получить гарантии релевантности, точности такого объяснения и его понятности для конкретного заинтересованного лица. Объяснимый искусственный интеллект (eXplainable AI, XAI) — новая, но быстрорастущая исследовательская дисциплина, в рамках которой разрабатываются и изучаются различные подходы, методы и инструменты, назначение которых состоит в формулировании конструктивных, точных и понятных объяснений.
Публикации выпуска касаются различных аспектов XAI и разных сфер применения. Прогресс в этой области, в частности, зависит от понимания ошибок, которые совершают пользователи. Номер открывает публикация «Объяснимые рекомендации и оценка доверия: систематические ошибки пользователя» (Explainable Recommendations and Calibrated Trust: Two Systematic User Errors), подготовленная группой авторов во главе с Мохаммадом Найсехом (Mohammad Naiseh). Они описывают методологию понимания ошибок «калибровки доверия», когда пользователи либо чрезмерно доверяют заключениям системы искусственного интеллекта, следуя неверным рекомендациям, либо отвергают правильные решения. Оценка уровня доверия к выводам человека или машины — нормальная часть процесса принятия решений. Но факторы, на которые полагаются пользователи при такой оценке, в случае человека и искусственного интеллекта различаются, в связи с чем и требуется понимание принципов «калибровки» доверия.
Саил Део (Sahil Deo) и Неа Самир Сонтакке (Neha Sameer Sontakke) стали соавторами статьи «Применимость, понимание пользователем и восприятие объяснений сложных систем поддержки принятия финансовых решений» (Usability, User Comprehension, and Perceptions of Explanations for Complex Decision Support Systems in Finance: A Robo-Advisory Use Case). Авторы обсуждают возможности представления объяснений с целью повышения их понятности для пользователя. В рассмотренном случае пользователи отдавали предпочтение частичному обзору модели с глобальной точки зрения, и их больше устраивало, когда сложные объяснения имели четкую структуру. Структурированный подход обеспечил повышение доверия к системе. Представленная в публикации схема объяснения с нескольких точек зрения может найти применение в инвестиционном консалтинге с учетом растущего использования искусственного интеллекта в этой сфере.
В публикации «Объяснимое машинное обучение для обнаружения мошенничества» (Explainable Machine Learning for Fraud Detection) группы авторов во главе с Исмини Психулой (Ismini Psychoula) подчеркивается важность анализа с целью выработки компромиссного решения по обеспечению объяснимости работы систем реального времени. Например, лучший в теории метод объяснения не всегда может быть самым подходящим для задачи, требующей высокой скорости решения: авторы показывают, что в некоторых случаях лучше использовать сочетание нескольких методов объяснения. Подчеркивается, что проектировщикам важно понимать характеристики различных подходов к обеспечению объяснимости, чтобы знать, каким образом применять их на практике. Как и во многих других областях, универсального подхода здесь нет, так что вместо поиска наилучшего следует определить, какой подойдет для конкретного случая и соответствующей аудитории.
Публикация «Объяснимый искусственный интеллект для систем обнаружения отказа холодильных установок» (Explainable AI for Chiller Fault-Detection Systems: Gaining Human Trust) Сешадри Сринивасана (Seshadhri Srinivasan) и др. посвящена методам обеспечения объяснимости для промышленных систем и ситуаций, когда человек взаимодействует с машиной при диагностике отказов. Авторы показывают, как с помощью методов XAI можно ускорить обнаружение дефектов при наладке систем кондиционирования воздуха, когда интеллектуальные средства применяются для содействия людям, инспектирующим оборудование и принимающим решения о вероятном отказе оборудования в ближайшем будущем. Применение XAI способствует повышению точности оценки влияния дефекта, уменьшению количества дефектов и оптимизации планирования технического обслуживания.
Другой аспект взаимодействия человека и систем ИИ обсуждается в статье «Автономные исследования и миссия ExoMars: машинное обучение помогает искать жизнь на Марсе» (Science Autonomy and the ExoMars Mission: Machine Learning to Help Find Life on Mars), подготовленной Викторией Дапоян (Victoria DaPoian) с соавторами. Миссии исследований космоса предполагают поиск ответов на вопросы открытого типа, а не бинарные, поэтому заранее продуманные решения есть не всегда. Системы, применяемые в этой области, должны рекомендовать план действий, которые с достаточной вероятностью обеспечат получение полезных данных. Авторы рассматривают проблему ведения исследований в автономном режиме и задачу объединения выводов машины и человека с целью не только поиска ответов на вопросы, но и постановки новых вопросов.
Андреас Хольцингер (Andreas Holzinger) и Хеймо Мюллер (Heimo Muller) опубликовали статью «Человечный искусственный интеллект: интерфейсы, обеспечивающие объяснимость и понимание работы медицинских систем искусственного интеллекта» (Toward Human — AI Interfaces to Support Explainability and Causability in Medical AI). В ней представлены идеи по поводу измерения качества объяснения искусственного интеллекта в режиме реального времени: предлагается оценивать реакцию людей с помощью датчиков и использовать эти сведения для уточнения объяснений. Применение интерфейса «человек — искусственный интеллект» для улучшения объяснимости работы искусственного интеллекта показано на примере процедуры гистологического исследования тканей.
Ноябрьский номер Computer посвящен кибербезопасности и доверию. Очередь ожидающих публикации работ на эти ключевые темы мира ИТ нескончаема, но для этого выпуска были отобраны лишь пять статей.
Номер открывает статья Малкольма Шора (Malcolm Shore) и соавторов «Нулевое доверие: суть, методы, причины, срочность» (Zero Trust: The What, How, Why, and When). Авторы отмечают появление двух конкурирующих направлений в сообществе информационной безопасности: «технологии, заслуживающие доверия» и «политика нулевого доверия». В публикации приводится обзор основополагающих концепций для обоих случаев и показано, что на самом деле два подхода взаимно дополняют друг друга, позволяя сформировать более связное и точное представление о доверии.
Просанта Гоуп (Prosanta Gope) и Биплаб Сикдар (Biplab Sikdar) стали соавторами статьи «Сравнительное исследование парадигм проектирования PUF-протоколов безопасности для устройств Интернета вещей» (A Comparative Study of Design Paradigms for PUF-Based Security Protocols for IoT Devices: Current Progress, Challenges, and Future Expectation). В публикации подчеркивается роль аутентификации устройств в обеспечении безопасности Интернета вещей. Устройства, размещенные в общественных местах, подвержены физическим воздействиям и атакам клонирования, в связи с чем авторы разъясняют возможность обеспечения более высоких уровней безопасности с помощью физически неклонируемых функций (Physically Unclonable Function, PUF), которые отличаются минимальными требованиями к вычислительным возможностям устройств.
Публикацию «Безопасность облачных приложений: риски, возможности и трудности защиты от эволюционирующих атак» (Cloud-Native Application Security: Risks, Opportunities, and Challenges in Securing the Evolving Attack Surface) подготовили Максим Чернышев (Maxim Chernyshev), Зубэр Бейг (Zubair Baig) и Шерали Зиделли (Sherali Zeadally). Отмечена повышенная вероятность компрометации облачных приложений в связи с изменчивостью угроз, подчеркивается, что для более полной защиты таких приложений требуется комплекс методов, представлена модель поставки облачных приложений. Приводится обзор современных методов обеспечения безопасности приложений, их преимуществ и недостатков.
В статье «Hack3D: краудсорсинг оценки защищенности цифрового производства» (Hack3D: Crowdsourcing the Assessment of Cybersecurity in Digital Manufacturing) группы авторов во главе с Майклом Линаресом (Michael Linares) обсуждается уязвимость цифровых производственных систем для физических и электронных атак. Приводятся доводы в пользу применения статистических методов для оценки вероятности компрометации систем безопасности. Подводятся итоги серии конкурсов Hack3D, направленных на проверку защищенности процессов работы с САПР и АСУТП методом послойной печати, отмечается, что в результате подобных хакатонов могут выявляться атаки принципиально новых типов.
Завершает выпуск статья Кристофа Эберта (Christof Ebert) и Раскила Рэя (Ruschil Ray) «Формальная модель отслеживаемости для эффективной валидации безопасности» (Toward a Formal Traceability Model for Efficient Security Validation). В ней описывается практическое применение предложенной модели при тестировании медицинской киберфизической системы на проникновение методом серого ящика. Подчеркивается, что формальное моделирование отслеживаемости в UML-средах способствует повышению результативности и эффективности тестов.
Александр Тыренко (shoorah@osp.ru) — независимый автор (Москва).
