Компания Aestetic Integration, специализирующаяся на анализе безопасности и прозрачности алгоритмов, применяемых на финансовых рынках, анонсировала проект Imandra Contracts – компания называет его первой в мире платформой формальной верификации смарт-контрактов, основанных на блокчейне.

Анонс был сделан на конференции DevCon-2 в Шанхае.

В программном обеспечении для финансовых рынков Imandra Contracts использует последние достижения в области искусственного интеллекта, математики и компьютерного моделирования. Компания ставит перед собой цели обеспечения прозрачности в разработке и регулировании смарт-контрактов.

Сделано для Эфириума

В качестве пилотного проекта новой облачной платформы выбрана сеть Эфириума. Говорит доктор Грант Пассмор (Grant Passmore), исполнительный директор и сооснователь Aestethic Integration:

Imandra – инструмент для анализа смарт-контрактов, он помогает пользователям понять, что они делают, зачем, и что может сработать не так, как задумано.

В разработке Imandra мы применяем последние достижения формальной верификации - области, в которой сочетаются исследования искусственного интеллекта, моделирование и математика. Наша цель - исследование всех возможных последствий исполнения смарт-контрактов.

Платформа поможет пользователям обнаруживать и исправлять аномалии в финансовых алгоритмах, а также выявлять возможные источники опасности до того, как они смогут повредить бизнесу. Полная приватность пользователей обеспечивается использованием облачного сервиса.

Банки уже пользуются сервисом Imandra

Пассмор отметил, что ряд крупных инвестиционных банков уже использует Imandra для анализа своих финансовых алгоритмов (речь идет пока именно о финансовых алгоритмах, а не о смарт-контрактах). Он напомнил, что Aestethic Integration стала победителем конкурса «Будущее Финансов», организованного банком UBS в 2015 году; темой конкурса был анализ соответствия требованиям регуляторов практики «темных пулов».

Теперь Imandra Contracts впервые переносит свои инструменты на технологии блокчейна.

Совместимость платформы – высочайший приоритет для Aestethic Integration, подчеркнул Пассмор. 

«Мы разрабатываем версии Imandra Contracts для многих платформ смарт-контрактов на блокчейне. Однако, мы начинаем с платформы "Эфириум", поскольку его виртуальная машина лучше всего детализирована (см. Желтую книгу), кроме того, учитывая недавние события, сообщество Эфириума лучше всех осознает необходимость формальной верификации».

Вопрос по поводу TheDAO

«Уязвимость, которая привела к взлому смарт-контракта TheDAO, как нельзя более ярко высветила крайнюю необходимость в более тщательном анализе смарт-контрактов финансовой отрасли», – говорит Пассмор, – «Урок TheDAO предельно ясен: Разработка смарт-контрактов должна стать инженерной дисциплиной, более похожей на разработку алгоритма контроля критических процессов, чем на веб-приложение».

Предотвратила бы Imandra Contracts взлом TheDAO?

«Точный ответ дать невозможно», – ответил Пассмор на вопрос в интервью. 

«Давайте перефразируем вопрос так: «Могла ли Imandra Contracts предотвратить взлом TheDAO»? Тогда ответ будет «Да». 

Технически, мы можем обозначить причины, приведшие к взлому как цели верификации, и запустить Imandra для автоматической проверки широкого класса смарт-контрактов на эти проблемы»

Финансовая отрасль и смарт-контракты

Пассмор не удивлен, что финансовая отрасль лидирует по суммам инвестиций в смарт-контракты.

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

Одно из наиболее востребованных направлений – оценка финансовых деривативов. Если банк переведет свою деятельность на смарт-контракты, через три года у него будет портфолио из сотен тысяч смарт-контрактов.

Такому банку понадобится оценка рисков, вычисление стандартных финансовых параметров и многое, многое другое. Это огромный рынок для анализа кода, лежащего в основе этих смарт-контрактов. Imandra Contracts активно работает в этом направлении.

Пассмор уверен, что и другие отрасли с жесткими стандартами безопасности, такие как изготовление оборудования или авионика, обязательно обратят внимание на формальную верификацию для обеспечения безопасности своих алгоритмов. 

«По мере того, как промышленность все больше адаптирует технологию блокчейна к своим надобностям, возрастает и необходимость в формализованных протоколах безопасности».

Уже сейчас Aesthetic Integration предлагает приложения для формальной верификации Imandra Markets и Imandra Venues.

  • Imandra Markets – система стандартных спецификаций алгоритма, которая упрощает разработку, тестирование и комплаенс приложений торговых систем.
  • Imandra Venues – анализирует торговые системы, биржи и темные пулы на предмет стабильности и соответствия регуляторным требованиям, что особенно актуально после недавних событий со штрафами и ограблениями. Эти события особенно подчеркивают высокую цену, которую приходится платить за пропущенные ошибки в алгоритмах.

В первой неделе октября Aestethic Integration планирует предварительную продажу доступа к Imandra Contracts. Первые пользователи смогут купить доступ в систему со значительным дисконтом.