A formal dynamic semantics of Java: an essential ingredient of Java security

• Autorzy: Debbabi M. , Tawbi N. , Yahyaoui H.
• Języki publikacji: EN

Abstrakty

EN

Security is becoming a major issue in our highly networked and computerized era. Malicious code detection is an essential step towards securing the execution of applications in a highly inter-connected context. In this paper, we present a formal definition of Java dynamic semantics. This semantics has been used as a basis to develop efficient, rigorous and provably correct static analysis tools and a certifying compiler aimed to detect and prevent the presence of malicious code in Java applications. We propose a small step operational semantics of a large subset for Java. The latter includes features that have not been completely addressed in the related work or addressed in another semantics style. We provide a fully-fledged semantic handling of exceptions, reachable statements, modifiers and class initialization.

Słowa kluczowe

EN

security; static analysis; certifying compilers; Java; dynamic semantics; operational semantics; small step semantics

PL

bezpieczeństwo; kryptografia

• Wydawca: Instytut Łączności - Państwowy Instytut Badawczy
• Czasopismo: Journal of Telecommunications and Information Technology
• Rocznik: 2002
• Tom: nr 4
• Strony: 81--120
• Opis fizyczny: Bibliogr. 23 poz., tab.

Twórcy

autor

Debbabi M.

autor

Tawbi N.

autor

Yahyaoui H.

• Panasonic Information, Networking Technologies Laboratory, Two Research Way, Princeton, New Jersey, USA,