Abstract Certification of Global Non-interference in Rewriting Logic - Formal Methods for Components and Objects - page 119

Table 1. Code measures, certificate sizes, and generation times

Code Examples → 1 2 3 4 5

↓
Code size in LOC 27 31 48 80 117
Code size in bytes 869 924 1981 3305 3504
Code cyclomatic complexity 1 1 4 16 192
Full Cert. size (Kb) 1134 1251 4223 10619 24176
Red. Rules Cert. size (Kb) 6.1 6.3 21.1 47.1 21.3
Red. Labels Cert. size (Kb) 1.8 1.8 2.6 3.7 5.2
Full Cert. Gen. Time (ms) 10408 23574 29482 45709 84331
Red. Rules Cert. Gen. Time (ms) 7057 7030 7527 8215 9547
Red. Labels Cert. Gen. Time (ms) 7030 6700 7190 8198 9537

Experiment Measures

abstract Java semantics specification, which is made available to the code con-
sumer, the certificate can be unexpensively checked on the consumer side by
any standard rewrite engine by means of a rewriting process that can be very
simplified. Actually, it suces to check that each abstract rewriting step in the
certificate is valid and that no rewriting chain has been disregarded, which essen-
tially amounts to using the matching infrastructure available within the rewriting
engine. Note that, according to the different treatment of rules and equations
in Maude, where only transitions caused by rules create new states in the space
state, an extremely reduced certificate can be delivered by just recording the
rewrite steps given with the rules, while the rewritings using the equations are
omitted.
The abstract certification methodology described here has been implemented
in Maude 4 . The prototype system offers a rewriting-based program certifica-
tion service, which is able to analyze global confidentiality program properties
related to non-interference. Our certification tool can generate three types of cer-
tificates: (i) the full certificates consist of complete rewriting sequences including
all rewrite steps; (ii) the reduced rules certificates only contain the rewrite steps
that use rules; and (iii) the reduced labels certificates only record the labels of
the used rules.
In Table 1, we analyze three key points for the practicality of our approach:
the size and complexity of the program code, the size of the three types of
certificates, and the certificate generation times. The running times are given
in milliseconds and were averaged over a sucient number of iterations. We
considered three code measures, the code size in LOC (lines of source code), the
code size in bytes, and the cyclomatic complexity, which counts the execution
paths of a program. The experiments were performed on a laptop with a Pentium
M 1.40 GHz processor and 0.5 Gb RAM.
Program 1 consists mainly of a simple non-interferent code example borrowed
from [23]. The program has been structured into two classes. The first class has
one secret variable and one public variable, a constructor method, two get meth-
ods, and a method that contains the non-interferent piece of code of [23]. The
second class is the main class with four method invocations. Similarly, program 2

4 The tool is provided with a Web interface written in Java and is publicly available
at http://www.dsic.upv.es/users/elp/toolsMaude/GlobalNI.hml