Along the years, software systems have inevitably grown in scale, functionality and, more in general, in complexity, augmenting the likelihood of errors and defects. Ensuring the correctness of the software has always been a critical problem. A major goal of software analysis is to enable developers to construct systems that operate reliably despite this complexity.
Furthermore, recently new introduced technologies for generating and executing code dynamically in virtual ambient have increased the complexity of the testing practice more. Nevertheless the features offered by the dynamic environments make them widespread.
In our work we extend the analysis process to make it cover untrusted code not known at load-time. We deal both with situations where the untrusted code is supplied by third party authors (e.g. a typical plug-in architecture), and with situations where the application itself will generate untrusted code at run-time. In the seminary a particular formal specification language will be exposed. We intend to attach the code specification to the object code itself as meta-data. Finally, through the reflection in Virtual Machines, we are then able to inspect the attached specifications to inject at run-time code for verification