jayhorn

владелец
депутат

Java и Horn Claouses

Jayhorn - это инструмент проверки программного обеспечения для Java. Джейхорн пытается найти доказательство того, что определенные плохие штаты в программе Java никогда не могут быть достигнуты. Эти плохие состояния определяются путем добавления утверждений времени выполнения (где могут быть сгенерированы некоторые утверждения, например, что ссылка на объект не должна быть нулевой до получения обращения).

Джейхорн пытается ошибиться на стороне точности, которая является, когда он не может доказать, что утверждение всегда удерживается, оно будет утверждать, что утверждение может быть нарушено (это называется обоснованностью). Jayhorn в настоящее время является звуком (модульные ошибки) для Java, которая использует один поток, не имеет динамической загрузки класса и не выполняет сложные операции в статических инициализаторах.

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

Присоединяйтесь к чату

Быстрый гид

./gradlew assemble
java -jar jayhorn/build/libs/jayhorn.jar -help
java -jar jayhorn/build/libs/jayhorn.jar -j example/classes -solution -trace

Зодовое утверждение

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

Наш анализ не имеет полностью звуковой обработки следующих функций:

• JNI, неявные вызовы метода (финализаторы, инициализаторы класса, поток. <int> и т. Д.)
• целое число переполнений
• исключения и поток, связанные с этим
• API Reflection (например, Method.invoke (), class.newinstance)
• вызываледамскую
• генерация кода во время выполнения, динамическая загрузка
• разные классовые погрузчики
• Ключевые нативные методы (Object.Run, Object.Doprivileged)

Это утверждение было произведено с генератором заявлений о прослушивании от Soundity.org.

Лицензии

Джейхорн открыт и распределен по лицензии MIT.

Библиотеки, используемые в Jayhorn, включают, в частности:

• Сажа, которая распределяется в LGPL 2.1 или более поздней версии.
• Eldarica, которая распространяется по лицензии BSD.
• Принцесса, которая распределяется в LGPL 2.1 или более поздней версии.

Благодарности и отказ от ответственности

Джейхорн частично финансируется:

• АФРЛ КОНТРАКТ № FA8750-15-C-0010.
• DARPA в соответствии с соглашением FA8750-15-2-0087
• Награда NSF № 1422705
• Грант Шведского исследовательского совета 2014-5484

Любые мнения, выводы и выводы или рекомендации, высказанные в этом материале, являются мнениями автора (-ов), не обязательно отражают взгляды AFRL, DARPA, NSF или шведского исследовательского совета.