Отладчик Space, разработанный в Массачусетском технологическом институте, пользуется особенностями фреймворка Ruby on Rails, в котором все операции, даже самые простые, заданы в библиотеках. Разработчики Space переписали библиотеки Ruby on Rails таким образом, чтобы реализованные в них операции описывали собственное поведение на логическом языке. В результате интерпретатор Rails превращается в инструмент статического анализа: при запуске программы на Rails с помощью интерпретатора тот генерирует формальное построчное описание работы программы с данными.
Процедуры обращения к данным сопоставляются с логической моделью, которая диктует, какие операции и при каких условиях допускается выполнять. Сравнивая описания, сгенерированные «взломанными» библиотеками, с моделью, Space автоматически определяет, отвечает ли ей программа; если нет, то в ней вероятно присутствие бреши безопасности.
В процессе испытаний на 50 популярных веб-приложениях система нашла 23 не диагностированных прежде уязвимости, причем на анализ отдельно взятой программы у Space ушло не больше 64 секунд.
