Information Technology Reference
In-Depth Information
notions in order to provide adequate methods for studying properties of com-
plex systems by analyzing the properties of computations that are conveyed
among system sub-components. In this sense, GANI may provide a framework
for studying the relation between different and interacting entities which may be
reciprocally influenced by the action of computing, giving advanced techniques
for systematically classifying the information leakage in the lattice of abstrac-
tions. Moreover, the advantage of specifying different notions of non-interference
for sequential, concurrent and timed systems as GANI relies upon the possibil-
ity offered by abstract interpretation to systematically derive abstractions. This
paper does not contain any tool support for the analysis, clearly such a tool
would provide an evidence on how the framework can be used, and indeed this
problem deserves further work. However, the definition of a general schema for
defining security properties allows to study relationship among different prop-
erties. Moreover, by using a unique model and unique schema, parametric on
the security policy and on the computational system, it is possible to develop
more general theories which could then be applied to a number of definitions by
simply instantiating them, in the same spirit as [12].
References
1. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science,
126(2) (1994) 183-235
2. Barbuti, R., De Francesco, N., Santone, A., Tesei, L.: A notion of non-interference
for timed automata. Fundamenta Informaticae, 51 (2002) 1-11
3. Bell, D.E., LaPadula, L.J.: Secure computer systems: Mathematical foundations
and model. Technical Report M74-244, MITRE Corp. Badford, MA (1973)
4. Clark, D., Hankin, C., Hunt, S.: Information flow for algol-like languages. Com-
puter Languages, 28(1) (2002) 3-28
5. Cohen, E.S.: Information transmission in sequential programs.
Foundations of
Secure Computation (1978) 297-335
6. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system
by abstract interpretation. Theor. Comput. Sci., 277(1-2):47,103 (2002)
7. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static
analysis of programs by construction or approximation of fixpoints. Proc. of
Conf. Record of the 4th ACM Symp. on Principles of Programming Languages
(POPL '77). ACM Press, New York (1977) 238-252
8. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. Proc.
of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages
(
POPL '79
). ACM Press, New York (1979) 269-282
9. Denning, D.E., Denning, P.: Certification of programs for secure information flow.
Communications of the ACM, 20(7) (1977) 504-513
10. Focardi, R., Gorrieri, R.: A classification of security properties for process algebras.
Journal of Computer security, 3(1) (1995) 5-33
11. Focardi, R., Gorrieri, R.: Classification of security properties (part i: Information
flow). R. Focardi and R. Gorrieri, editors,
Foundations of Security Analysis and
Design
, volume 2171 of
Lecture Notes in Computer Science
. Springer-Verlag (2001)
12. Riccardo Focardi and Fabio Martinelli: A uniform approach for the definition of
security properties. World Congress on Formal Methods (1) (1999) 794-813
