Der Artikel führt eine neue formale Charakterisierung der Stapelsicherheit ein, die auf Konzepten der sprachbasierten Sicherheit basiert. Anstatt die Stapelsicherheit als monolithische Eigenschaft zu behandeln, wird sie in fünf Eigenschaften unterteilt: Integrität und Vertraulichkeit für den Aufrufer und den Aufgerufenen sowie eine wohlgeformte Kontrollflusskette.
Diese Formulierung wird durch eine bestimmte Klasse von Durchsetzungsmechanismen, die "lazy" Stapelsicherheits-Mikro-Richtlinien, motiviert, die es Funktionen erlauben, in die Frames anderer zu schreiben, aber die geänderten Stellen so markieren, dass der Besitzer des Frames darauf nicht zugreifen kann.
Die Eigenschaften gehen über bisherige formale Definitionen der Stapelsicherheit hinaus, indem sie Aufrufer- und Aufgerufenen-gespeicherte Register, Argumente, die auf dem Stapel übergeben werden, und Tail-Call-Elimination unterstützen. Die Autoren validieren die Eigenschaften, indem sie sie verwenden, um korrekte und inkorrekte Implementierungen der Mikro-Richtlinien von Roessler und DeHon mit eigenschaftsbasiertem Zufallstesten zu unterscheiden.
他の言語に翻訳
原文コンテンツから
arxiv.org
深掘り質問