В MIT разработали абсолютную защиту от компьютерных сбоев

Исследователи из лаборатории CSAIL (Computer Science and Artificial Intelligence Lab) Массачусетского технологического института (MIT) предложили надежное, по их мнению, решение для защиты от любых компьютерных сбоев. Их подход базируется на идее, что сами по себе отказы оборудования, дефекты программ или прерывания подачи питания это не проблема, проблема в их последствиях, а точнее, в потерянной или поврежденной информации.

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

«Крайне сложно гарантировать, что система будет восстанавливаться после сбоя в любой точке, слишко много различных причин для возможного сбоя, – пишет Николай Зельдович, один из трех профессоров информатики MIT, участвовавших в подготовке новой статьи. – Вам потребуется рассмотреть буквально каждую команду или каждую дисковую операцию и всякий раз спрашивать себя: а что если система откажет прямо сейчас? Что тогда?».

Тем не менее, авторы полны уверенности, что метод формальной верификации обеспечит нужные гарантии целостности – не высокоуровневой схемы, но конечного кода файловой системы. Для этого ими используется инструмент Coq – так называемый доказательный помощник (proof assistant), который предоставляет формальный язык описания систем и их взаимоотношений.

Продемонстрировать систему в действии ученые планируют на ACM Symposium on Operating Systems Principles, который состоится этой осенью. Математическое гарантирование сохранности данных, по их словам, это лучше всего, что могут сегодня предложить любые отказоустойчивых технологии, даже учитывая на сложность реализации и пока еще медленную работу нового алгоритма.