Abstracts of talks at the Winchesters IFIP WG1.3 meeting

Abstracts of talks at the Winchester IFIP WG1.3 meeting (September 3-4th, 2011)

1 - Peter Padawitz, Technical University of Dortmund
Many-sorted signatures presenting categories of co/algebras
Abstract:
The types of the functions of a traditional many-sorted signature Sig are restricted to the form s1 x ... x sn -> s. Non-trivial applications require the distinction of base sorts among all sorts. In the Sig-algebra approach, base components come as subsignatures, while F-co/algebras represent them as the constants functors among the constituents of F. In the case of several sorts taken from a set S, F is an endofunctor on Set^S. We introduce the notion of a signature Sig that captures most of those endofunctors that are practically relevant and have initial and/or final fixpoints. Sig consists of S, a finite set BS of base sets and function symbols f:e->e' where e and e' are type constructions over S and BS. f is interpreted as a natural transformation between the functors from Set^S to Set, which are denoted by e and e', respectively. We show how the elements of initial/final models of Sig can be represented as (equivalence classes of) terms, similarly or dually to the ones associated with traditional many-sorted signatures.

Here is an unfinished collection of notions and results on co/algebraic modeling, adapted to the syntax described above. It also includes well-known fundamentals of order theory, category theory and many-sorted predicate logic. Corrections and other comments are welcome!

2 - Kokichi Futatsugi, JAIST (Japan Advanced Institute of Science and Technology), slides
An Overview of Recent Research Activities around CafeOBJ
Abstract:
This talk gives an overview of recent research activities around CafeOBJ formal specification language system.

After giving some introductory remarks on formal methods, CafeOBJ, and proof scores, two major approaches of combining inference (a la theorem proving) and search (a la model checking) in verifications with proof scores are explained with instructive simple examples. The one is a sort of typical combination of abstraction which is proved by inference with proof score and search of limited state space after the abstraction. The other is combination of backward search (with inference) and forward search (with search) in finding counter-examples which is called Induction Guided Falsification.

An important theoretical achievement of formalization of sound and "complete" proof rules which underlie the proof score method is also explained.

URL of related papers and presentation:

related paper 1, web page for presentation of paper 1, related paper 2

3 - Carroll Morgan, University of New South Wales, slides
Refinement-oriented noninterference: Comparison of a qualitative and a quantitative model
[Joint work with] Annabelle McIver (Macquarie University), Larissa Meinicke (Macquarie University)
Abstract:
Qualitative vs quantitative semantics for noninterference: an evolution in parallel

The Shadow model for qualitative noninterference of sequential programs [a] is a denotational model, complete with a refinement relation that preserves both functional- and security properties (the latter within its terms of reference). It was derived from a series of "gedanken" experiments in program-refinement algebra, then applied to Kripke structures as used for logics of knowledge.

The Hyperdistribution model for quantitative noninterference [b] was later constructed with the Shadow in mind, but essentially independently. It turns out to have strong structural links to Hidden Markov Models.

The technical component of this talk will be to describe the two kinds of semantics, i.e. the Shadow- (qualitative, possibilistic) and Hyperdistribution- (quantitative, probabilistic) structures we have built for noninterference with a refinement partial order (ie an implementation order that respects secrecy). Unusually, the two models will be described in parallel (interleaved concurrency, not truly concurrent with two screens); in this way I will try to bring out their similarities and differences.

If time permits, an example will be given of the kind of program algebra that results, and how the qualitative- and quantitative algebras can work together.

[a] C.C. Morgan. The Shadow Knows: Refinement of ignorance in sequential programs.
Conference version in Proc. Math Prog Construction 2006, LNCS 4014:359-78, 2006.
Journal version in Science of Computer Programming, 74(8):629-653, 2009.

[b] Annabelle McIver, Larissa Meinicke, and Carroll Morgan.
Compositional closure for Bayes Risk in probabilistic noninterference.
ICALP'10 Part II, pages 223-235, 2010.

4 - Bernd-Holger Schlingloff, Humboldt University and Fraunhofer FIRST, Berlin, Germany, slides, paper
Specification and Modelling of Embedded Systems
Abstract:
We present work in the formalization of natural-language specifications in UML2, temporal logics, timed automata, and Spec#. We observe that the different languages lead to very different formalizations, and hence there is a need for a metric indicating the quality of a formalization.

5 - Alexander Kurz, University of Leicester,
Effective Syntax for Semantic Categories
Abstract:
In his AiML 2010 invited lecture, Martin Otto discussed how to obtain "concrete and effective syntax for a class of semantic structures", where his examples referred on the semantic side to the model theory of first-order logic and to modal logic on the syntactic side. Instead of model theory, we may as well look to category theory for such semantic structures. Of course, there is already a beautiful and well-developed theory of categorical logic. Recent efforts connecting coalgebras and modal logic can also be seen as part of the generic setting. But more semantic categorical structures are waiting to be explored. Further, structures coming from model theory and from category theory may also be combined.

6 - Andrzej Tarlecki, The University of Warsaw, slides
Compositional Property-oriented Semantics for Structured Specifications. Another Old Story (with a Few New Twists)
Abstract:
Working in an arbitrary institution, we discuss property-oriented semantics of specifications built using some collection of specification-building operations. As a typical example we consider the structured specifications built from flat specifications using union, translation and hiding. For such specifications we have the standard compositional proof system, which determines the standard property-oriented semantics assigning a theory to each structured specification. It is not complete (unless the underlying logic has interpolation and enjoys some other technical properties) but otherwise it is "as good as can be expected". In particular, it is sound, monotone (and hence compositional) and closed complete. The last property means that the semantics (and the corresponding proof system) allows us to deduce all true consequences for specifications built by applying any specification-building operation to argument specifications, assuming that there is no discrepancy between the classes of models of the argument specifications and the classes of models of their respective property-oriented meanings. This is a strong property which was believed to ensure that the semantics is "as strong as possible" without loosing soundness or compositionality. We question this claim and show that it holds assuming in addition that the semantics considered are theory-oriented, i.e., the sets of properties assigned to specifications are closed under consequence, as well as non-absent-minded, i.e., no axioms from flat specifications are omitted as properties. We sketch examples to show that neither of these requirements may be dropped. We generalise this study to the context of entailment systems, and show similar results and counterexamples.

7 - Mark Ryan, University of Birmingham (UK), paper
Modelling and verifying privacy properties of web systems
[Joint work with] Myrto Arapinis, Sergiu Bursuc (University of Birmingham)
Abstract:
We describe the protocol underlying a novel cloud-based conference management system that offers strong security and privacy properties. In our system, authors, reviewers and the conference chair interact through their web browsers with the cloud, to perform the usual tasks of uploading and downloading papers and reviews. In contrast with current systems, in our system the cloud provider does not have access to the content of papers and reviews, and moreover is unable to link authors, reviewers, and scores. We provide a prototype implementation of the system and performance results. We also express the protocol and its desired privacy properties in the language of ProVerif, and automatically prove that the properties hold.

8 - Lutz Schröder, DFKI GmbH, slides
Towards the Coalgebraic Guarded Fragment
[Joint work with] Daniel Gorín
Abstract:
The guarded fragment of first-order logic is in many respects closely related to modal logic in terms of model properties, expressivity, and complexity. We show that the binary guarded fragment is equivalent to a natural extension of the DL ALCHIO which provides additional expressive means for talking about the prestate. We then generalize some of the features relating to the prestate to the coalgebraic setting, and speculate on coalgebraic correspondents for the remaining features.

1 - Till Mossakowski, DFKI GmbH, slides
A structural hybrid logic for CSP and other process algebras
[Joint work with] Lutz Schröder
Abstract:
Based on Ichiro Hasuo's compositional semantics of GSOS-based process operators, we equip CSP with a compositional transition system semantics. Moreover, we develop a structural hybrid logic for specifying abstract requirements. These requirements can be successively refined to a design, thereby introducing CSP process operators (like parallel composition) - these are all available in the logic, until a pure CSP process is reached. The relation between CSP and the structural hybrid logic is formalised as an institution comorphism that embeds CSP into the logic.

10 - Dusko Pavlovic, Royal Holloway / University of London, slides
New directions in security by obscurity
Abstract:
Shannon sought security against the attacker with unlimited computational powers: *if an information source conveys some information, then Shannon's attacker will surely extract that information*. In their seminal paper "New directions in cryptography", Diffie and Hellman refined Shannon's attacker model by taking into account the fact that the real attackers are computationally limited. This idea was the stepping stone into modern cryptography.

Shannon also sought security against the attacker with unlimited logical and observational powers, expressed through the maxim that "the enemy knows the system". This view is still fully endorsed in modern cryptography. The popular formulation, going back to Kerckhoffs, is that "there is no security by obscurity", meaning that the algorithms cannot be kept obscured from the attacker, and that security should only rely upon the secret keys. In fact, modern cryptography goes even further than Shannon or Kerckhoffs in tacitly assuming that *if there is an algorithm that can break the system, then the attacker will surely find that algorithm*. The attacker is not viewed as an omnipotent computer any more, but he is still construed as an omnipotent programmer.

Attempting to lift the Diffie-Hellman refinement step from attacker's computational powers, to attacker's programming powers leads to questions of *logical complexity* of specification transformations, such as: Can we formally characterize logical complexity of the task involved of transforming one specification (e.g. of a system and its security requirements) into another specification (e.g. of an attack on that system, breaching the security requirements)?

11 - Pierre-Yves Schobbens, FUNDP University of Namur, slides
On-the-fly Strategy Synthesis for Event-Clock Linear Temporal Logic on Timed Games!
[Joint work with] Peter Bulychev, Barbara Di Giampaolo, Laurent Doyen, Gilles Geeraerts, Jean-Francois Raskin, Julien Reichert, Tali Sznajder
Abstract:
We present a tool for the synthesis of a real-time controller from a timed automaton describing the plant, and a goal expressed in a real-time linear temporal logic. It extends the UPPAAL-TIGA tool by accepting a richer temporal logic. The problem is EXPTIME-complete; so performance is a critical issue. Our on-the-fly algorithm is based on bounded synthesis.

12 - Corina Cirstea,University of Southampton, UK, slides, paper
Maximal Traces and Path-Based Coalgebraic Temporal Logics
Abstract:
This paper gives a general coalgebraic account of temporal logics whose semantics involves a notion of computation path. Examples of such logics include the logic CTL* for transition systems and the logic PCTL for probabilistic transition systems. Our path-based temporal logics are interpreted over coalgebras of endofunctors obtained as the composition of a computation type (e.g. nondeterministic or stochastic) with a general transition type. The semantics of such logics relies on the existence of execution maps similar to the trace maps introduced by Jacobs and co-authors as part of the coalgebraic theory of finite traces [1]. We consider both finite execution maps derived from the theory of finite traces, and a new notion of maximal execution map that accounts for maximal, possibly infinite executions. The latter is needed to recover the logics CTL* and PCTL as specific path-based logics.