Information Technology Reference
In-Depth Information
*OREDO3URWRFRO
352-(&7,21
$WGHVLJQWLPH
/2&$/35272&2/)256
/2&$/35272&2/)25&
/2&$/35272&2/)25$
ORFDO
SURWRFRO
2QOLQH:DOOHW
DW
&
UROH
6
UROH
&
UROH
$^
ORJLQLG
VWULQJ
SZ
VWULQJ
WR
$
FKRLFH
DW
$^
ORJLQBRN
IURP
$
UHF
/223^
DFFRXQWEDODQFH
LQW
RYHUGUDIW
LQW
IURP
6
FKRLFH
DW
&^
#DPRXQWEDODQFHRYHUGUDIW!
SD\SD\HH
VWULQJ
DPRXQW
LQW
WR
6
FRQWLQXH
/223
`
RU
^
TXLW
WR
6``
`
RU
^
ORJLQBIDLOHUURU
VWULQJ
IURP
$``
)60*(1(5$7,21
$WUXQWLPH
)60)256
)60)25$
9HULILFDWLRQ
352*5$0)256
352*5$0)25&
352*5$0)25$
Fig. 2.
Global specification to local runtime verification methodology
the initial message specifies which role it intends to play. Its monitor retrieves
the local specification based on the protocol name and the role. Fig. 2 gives the
local protocol and associated FSM for the client role C (we omit the protocols
for S and A). The FSM encodes the flow of local communication actions, with
transitions fired by the input and output of the permissible messasges.
Policy Validation.
The final level of verification enables the elaboration of
Scribble protocols using annotations (
@
<
...
>
in Fig. 1 and 2). The annotations
function as API hooks to the verification framework: they are not verified by
the MPST monitor itself, but delegated to a third-party engine. Various pol-
icy domains (e.g. security policies) can be enforced by integrating engines for
predicates on endpoint state, automata-based properties, etc., as extensions to
the core protocol monitor. Our current implementation uses a Python library for
evaluating basic predicates (e.g. the overdraft check in Fig. 1), which is sucient
for the application protocols we have developed with [11]. At runtime, the moni-
tor passes the annotation information, along with the FSM state information, to
the appropriate policy engine to perform the additional checks or calculations.
To plug in an external validation engine, our toolchain API requires modules for
parsing and evaluating the annotation expressions specified in the protocol.
3 Toolchain Requirements and Evaluation
3.1 Monitor Requirements
Positioning.
The network monitoring in our theory imposes
complete mediation
of communications: no communication action should have an effect unless the
