jayhorn

Master
Devel

Java- und Hornklauseln

Jayhorn ist ein Softwaremodell -Checking -Tool für Java. Jayhorn versucht einen Beweis dafür, dass bestimmte schlechte Zustände in einem Java -Programm niemals erreichbar sind. Diese schlechten Zustände werden durch das Hinzufügen von Laufzeitbehauptungen angegeben (wobei einige Behauptungen generiert werden können, z. B. dass eine Objektreferenz nicht null sein darf, bevor er zugegriffen wird).

Jayhorn versucht auf der Seite der Präzision zu irren, wenn es nicht in der Lage ist, zu beweisen, dass eine Behauptung immer gilt, wird behaupten, dass die Behauptung verletzt werden kann (dies wird als Fundualität bezeichnet). Jayhorn ist derzeit Sound (Modulo -Fehler) für Java, die einen einzelnen Thread verwenden, keine dynamische Klassenbelastung haben und keine komplexen Operationen in statischen Initialisierern durchführen.

Informationen zum Herunterladen und Ausführen von Jayhorn finden Sie auf unserer Website. Informationen darüber, wie Jayhorn implementiert wird, finden Sie in unserem Jayhorn Development -Blog.

Treten Sie dem Chat bei

Schnelle Anleitung

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

Eingehende Aussage

Dieses Projekt wurde im Geiste der Hunden durchgeführt. Beim Aufbau praktischer Programmanalysen ist es häufig erforderlich, Ecken zu schneiden. Um offen für Sprachmerkmale zu sein, die wir nicht unterstützen oder nur teilweise unterstützen, fügen wir diese eingehende Aussage an.

Unsere Analyse enthält keine vollständige Klanghandhabung der folgenden Funktionen:

• JNI, implizite Methodenaufrufe (Finalizer, Klasseninitialisierer, Thread. <Init> usw.)
• Ganzzahlüberlauf
• Ausnahmen und Fluss damit verbunden
• Reflexions -API (z. B. Methode.invoke (), class.Newinstance)
• angerufen
• Codegenerierung zur Laufzeit, dynamisches Laden
• Verschiedene Klassenlader
• Key Native Methoden (Object.Run, Object.Doprivilegiert)

Diese Aussage wurde mit dem Soundiness Statement Generator von Soundiness.org produziert.

Lizenzen

Jayhorn ist Open-Source und verteilt unter MIT-Lizenz.

In Jayhorn verwendete Bibliotheken gehören insbesondere:

• Ruß, der unter LGPL 2.1 oder höher verteilt ist.
• Eldarica, das unter BSD -Lizenz verteilt ist.
• Prinzessin, die unter LGPL 2.1 oder höher verteilt ist.

Anerkennung und Haftungsausschlüsse

Jayhorn wird teilweise finanziert von:

• AFRL-Vertrag Nr. FA8750-15-C-0010.
• DARPA unter Vereinbarung FA8750-15-2-0087
• NSF Award Nr. 1422705
• Der schwedische Forschungsrat Grant 2014-5484

Alle Meinungen, Ergebnisse und Schlussfolgerungen oder Empfehlungen, die in diesem Material geäußert werden, sind nicht unbedingt die Ansichten von AFRL, DARPA, NSF oder des schwedischen Forschungsrates widerspiegeln.