Formalizing workflows partitioning over federated clouds: multi-level security and costs

Abstract

This paper presents an formalization of federated cloud workflows using the Z notation. It is an abstract specification with properties of interest being observed by the possible deployments, which are symbolically calculated by the Z/EVES theorem prover. Mathematical rules are used to define these properties by restricting valid options for security, cost, dependability, etc. A Haskell implementation of these proved properties is also presented. We have a Haskell implementation of the approach that is used to generate valid workflow deployment options, given the user workflow input and the security and cost properties of interest. The result is a set of (sub)-workflows as GraphWiz files respecting these properties.

Keywords:

• federated clouds
• formal proof
• Bell–LaPadula
• Haskell
• Z/EVES

2010 AMS Subject Classifications:

• 68R06
• 03C06

Acknowledgements

This work was funded by the Research Councils UK Social Inclusion through the Digital Economy project EP/G066019/1 (SiDE) and by EPSRC grant EP/H024204/1 (AI4FM). We would also like to thank Cliff Jones and Gudmund Grov for discussions on various versions of our model.

Notes

1. The sources of this paper are formally analysed.

2. See AI4FM at www.ai4fm.org.

3. We use this font for mathematical references in the text.

4. Formally, a relation R∈X ↔ Y is the same as R∈ℙ (X oss Y).

5. The paper 12 has a Haskell implementation.

6. We use the Community Z Tools (CZT), see details at http://czt.sourceforge.net.

7. Decorated (dashed) schema names, decorate all its fields.

8. In Z, input variable names have a ‘?’ suffix by convention.

9. Schemas allow access to fields of w: it has schema type WF.

10. In Z, output names have ‘!’ suffixes by convention.

11. www.e-sciencecentral.org.

12. To avoid confusion, schemas/types with similar names as in the previous section are given an EXT suffix.

13. The relational image R (|S|) projects all elements of the relation (or set of pairs) R where S is a set in the domain of R. More specifically, if R is a function f and x is in its domain, then f (| {x} |)={f (x)}.

14. See http://www.graphviz.org/.

15. Technically, it builds a lattice: a partially ordered set satisfying various important mathematical properties useful for reasoning about the programme.

16. See http://isabelle.in.tum.de/haskabelle.html.

17. See AI4FM www.ai4fm.org.