Arrow Research search

Author name cluster

Luca Martini

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

TCS Journal 2010 Journal Article

Using abstract interpretation to add type checking for interfaces in Java bytecode verification

  • Nicoletta De Francesco
  • Giuseppe Lettieri
  • Luca Martini

Java interface types support multiple inheritance. Because of this, the standard bytecode verifier ignores them, since it is not able to model the class hierarchy as a lattice. Thus, type checks on interfaces are performed at run time. We propose a verification methodology that removes the need for run-time checks. The methodology consists of: (1) an augmented verifier that is very similar to the standard one, but is also able to check for interface types in most cases; (2) for all other cases, a set of additional simpler verifiers, each one specialized for a single interface type. We obtain these verifiers in a systematic way by using abstract interpretation techniques. Finally, we describe an implementation of the methodology and evaluate it on a large set of benchmarks.

Details DOI

I&C Journal 2007 Journal Article

Instruction-level security analysis for information flow in stack-based assembly languages

  • Nicoletta De Francesco
  • Luca Martini

We propose a method to analyze secure information flow in stack-based assembly languages, communicating with the external environment by means of input and output channels. The method computes for each instruction a security level for each memory variable and stack element. Instruction-level security analysis is flow-sensitive and hence is more precise than other analyses, such as standard security typing. Instruction-level security analysis is specified in the framework of abstract interpretation. We define concrete operational semantics which handles, in addition to execution aspects, the flow of information of the program. The basis of the approach is that each value is annotated by a security level and that the abstract domain is obtained from the concrete one by keeping the security levels and forgetting the actual values. Operand stack are abstracted as fixed-length stacks of security levels. An abstract state is a map from instructions to abstract machine configurations, where values are substituted by security levels. The abstract semantics consists of a set of abstract rules manipulating abstract states. The instruction-level security typing can be performed by an efficient fixpoint iteration algorithm, similar to that used by bytecode verification.

Details DOI
v2026.09.13