Системные сбои, отключения электричества, вспышка молнии – множество факторов могут лишить пользователя итогов его работы, которые он не успел сохранить в файл на своем жестком диске или в "облаке". В Массачусетском технологическом институте (США) предлагают новый способ борьбы с этой проблемой.

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

Для них группа Николая Зельдовича из МТИ и разработала новый тип формального верифицирования, позволяющий создать файловые системы, неуязвимые к системным сбоям, какими бы причинами они ни вызывались. Использование формальной верификации в файловых системах далеко не новость. Однако до недавних пор она велась лишь на ''верхних программных уровнях''. Кроме того, использовавшиеся ранее подходы были адаптированы лишь к некоторым операционным системам, что не позволяло широко использовать их на других OS.

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

Сейчас Зельдович работает над ее оптимизацией и выработкой подхода, который позволил бы применять столь же полную низкоуровневую формальную верификацию на других ОС. Ульфар Эрлингсон, ведущий менеджер Google по вопросам безопасности, уже отметил, что новая работа МТИ вполне может стать основой для создания широкого спектра устойчивых к потере данных приложений как на мобильных, так и на стационарных устройствах.

Источник: Агентство по инновациям и развитию