Showing posts with label Proof. Show all posts
Showing posts with label Proof. Show all posts

Monday, 19 May 2014

Foundations of Privacy - Another Idea

This got triggered by a post on LinkedIn about what a degree in privacy might contain. I've certainly thought about this before, at least in terms of software engineering, and even have a whole course that could be taken over a semester ready to go.

Aside: CMU has the "World's First Privacy Engineering Course": a Master of Science in Information Technology—Privacy Engineering (MSIT-PE) degree. So, close, but a major university here in Finland turned down the chance to create something similar a few years back...

That aside, I've been wondering about how to present they various levels of things we need to consider to properly define privacy and put it on strong foundations. Though in the guise of information theory we already have this, though admittedly Shannon's seminal work from the 1930's is maybe a little too deep. On the other hand understanding concepts such as channels, entropy are fundamental building blocks, so maybe they should be there along with privacy law - now that would make some course!

Even just sketching out areas to present and what might be contained therein...how about this, even if a linear map from morality to mathematics is too constraining?



There are missing bits - we still have a  semantic gap between the "legal world" and the "engineering world"; parts that I'm hoping that things such as the many conferences, academic works and books such as the excellent Privacy Engineer's Manifesto and Privacy Engineering will play a role in defining. Maybe the semantic gap goes away once we start looking at this...is there even a semantic gap? 

However, imagine for a moment starting anywhere in this stack and working up and down and keeping everything linked together in the context of privacy and information security. Imagine seeing the link between EU privacy laws and type theory, or between the construction of policies and entropy, the algebra of HIPAA, a side course in homotopy type theory and privacy...maybe with that last one I'm getting carried away, but, this is exactly what we need to have in place.

Each layer provides the semantics to the layer above - what do our morals and ethics means in terms of formalised laws, what do laws mean in terms of policies, what do policies mean in terms of software engineering structures, and down to the core mathematics and algebras of information.

Privacy and privacy engineering in particular almost has everything: law, algebra, morals, ethics, semantics, policy, software, entropy, information, data, BigData, Semantic Web etc etc etc. Furthermore, we have links to areas such as security, cryptography, economic theory etc!

Aren't these the very things any practitioner of privacy (engineering) should know, or at least have knowledge of? Imagine if lawyers understood information theory and semantics, and, software engineers understood law? 

OK, so there might be various ways of putting this stack together, competing theories of privacy etc, but that would be the real beauty here - a complete theory of privacy from the core mathematics through physics, computation, type theory, software engineering, policies, law and even ethics and morals.

But again, no more naivety, no more terminological or ontological confusions, policies and laws being traceable right down to the computation structures and code. Quite a tall order, but such a course bringing all these together really would be wonderful...

And wouldn't that be something!

Wednesday, 30 October 2013

Diagrams Research

For a number of years I and some colleagues have worked closely with the University of Brighton's Visual Modelling Group using their work on diagrammatic methods of modelling and reasoning. One of the areas where we've had quite a nice success is in modelling aspects of information privacy [1] with some particularly useful and beautiful and natural representations of complex ideas and concepts.

Another area has been in the development of ontologies and classification systems - something quite critical in the area of information management and privacy. Some of this dates back to work we made with the M3 project and the whole idea of SmartSpaces incorporating the best of the Semantic Web, Big Data etc.



We've gained quite a considerable amount of value out of this relatively, simple industrial-academic partnership. A small amount of funding, no major dictatorial project plans but just letting the project and work develop naturally, or even if you like, in an agile manner, produces some excellent, useful and mutually beneficial results.

Indeed not having a project plan but just a clearly defined set of things that we need addresses and solved (or just tackled - many minds with differing points of view really does help!) means that both partners: the industrial and the academic, can get on with the work rather than battling an artificial project plan which becomes increasingly irrelevant and industrial focus and academic ideas change over time. Work continues with more ontology engineering in the OntoED project.

References:
  1. I. Oliver, J. Howse, G. Stapleton. Protecting Privacy: Towards a Visual Framework for Handling End-User Data. IEEE Symposium on Visual Languages and Human-Centric Computing, San Jose, USA, IEEE, September, to appear, 2013.
  2. I. Oliver, J. Howse, G. Stapleton, E. Nuutila, S. Torma. Visualising and Specifying Ontologies using Diagrammatic Logics. In proceedings of 5th Australasian Ontologies Workshop, Melboune, Australia, CRPIT vol. 112, December, pages 37-47, 2009. Awarded Best Paper
  3. J. Howse, S. Schuman, G. Stapleton, I. Oliver. Diagrammatic Formal Specification of a Configuration Control Platform. 2009 Refinement Workshop, pages 87-104, ENTCS, November, 2009.
  4. I. Oliver, J. Howse, G. Stapleton, E. Nuutila, S. Torma. A Proposed Diagrammatic Logic for Ontology Specification and Visualization. 8th International Semantic Web Conference (Posters and Demos), October, 2009.
  5. J. Howse, G. Stapleton, I. Oliver. Visual Reasoning about Ontologies.International Semantic Web Conference, China, November, CEUR volume 658, pages 5-8, 2010.
  6. P. Chapman, G. Stapleton, J. Howse, I. Oliver. Deriving Sound Inference Rules for Concept Diagrams. IEEE Symposium on Visual Languages and Human-Centric Computing, Pittsburgh, USA, IEEE, September, pages 87-94, 2011.
  7. G. Stapleton, J. Howse, P. Chapman, I. Oliver, A. Delaney. What can Concept Diagrams Say? Accepted for 7th International Conference on the Theory and Application of Diagrams 2012, Springer, pages 291-293, 2012.
  8. G. Stapleton, J. Howse, P. Chapman, A. Delaney, J. Burton, I. Oliver.Formalizing Concept Diagrams. 19th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing, Knowledge Systems Institute, to appear 2013.

Monday, 16 April 2012

LoD 2012: Layout of Diagrams 2012

LOD 2012

3rd International Workshop on Layout of Diagrams 

Diagrams are an effective means of conveying a wide variety of different sources of information. They play a vital role in communication at many levels, and the quality of diagram layout effects the ease of communication. Creating task-adequate layouts is surprisingly difficult, and the cognitive factors involved are often not very well understood. The automatic generation of diagrams is essential for many tasks such as the presentation of multiple views of large scale data sets. In many domains, tool support is not satisfactory. The workshop aims to bring together different communities that can learn from each other, both within different academic disciplines and between academia and industry.
We solicit original submissions related to diagram layout, in areas including, but not limited to, the following areas:
  • Layout algorithms ;
  • Layout design styles, guidelines and patterns;
  • Automatic diagram generation and transformation techniques;
  • Visual language theory (e.g. quality metric development) ;
  • Visualisation of constraints, algorithms, and tools;
  • Cognitive or empirical research on diagram layout;
  • Diagram layout for diagrammatic reasoning, knowledge representation, etc;
  • Application areas (e.g. system modelling, ontology visualisation, etc, with an emphasis on layout requirements and benefits).
All diagram types fall within the scope of the workshop series (e.g. graphs, hypergraphs, Euler diagrams, maps, knot diagrams, etc). Of particular interest is research and techniques that may encourage interaction and knowledge transfer between fields. However, for this instalment of the workshop series, we particularly encourage submissions that have a software engineering orientation (e.g. those within UML, IDEF or ARIS), building on the success of two previous workshops at VL/HCC on the Layout of Software Engineering Diagrams (LED).

The proceedings of this workshop will be published in the journal of Electronic Communications of the EASST (TBC). All papers must conform to the ECEASST format. All papers must be submitted electronically in the PDF format via the EasyChair submission system. Each submission will be reviewed by 3 reviewers, as usual.

The intention is that after the workshop the authors of the best papers will be invited to submit a revised and significantly extended version of their article to a special issue of a sutiable journal (e.g. Journal of Visual Languages and Computing or the journal of Software and Systems Modeling).

Important Dates

  • Abstract Submission: June 11th, 2012
  • Paper Submission: June 18th, 2012
  • Notification to Authors: August 8th, 2012
  • Camera Ready Submission: August 30th, 2012
  • Workshop Dates: Oct 4th, 2012

 

 

Saturday, 25 February 2012

The Requirement of using Formal Methods

A very interesting posting by way of LtU about the ethics, morals and necessity of using formal methods when developing software: When Formal Systems Kill: Computer Ethics and Formal Methods by Darren Abramson and Lee Pike. I'll cherry pick two quotes that stood out for me from this paper: the first being:

How to mathematically model formal systems and their environments. Unlike other engineering artifacts that are mathematically-modelled (bridge stresses, aircraft aerodynamics, etc.), many concepts in computer science are brand new, and a research challenge is simply how to mathematically model these concepts. Such concepts of course include modelling software and hardware and the environments in which they operate.

The fact that much of the work we're doing in the computer science area is brand appears curious, but if you think that in many cases the mere act of formalising something reveals how little is understood about the underlying theory. So while a new design of bridge can be built, it still uses well known and (importantly!) well understood underlying theories to verify and validate its design. Compare this to situations that arise in computer science, eg: the formalisation of policy structures for privacy, or the design of a space-based semantic web inspired, personal cloud and you quickly realise how little we know.

Privacy is an interesting issue, for example we have many groups proposing "engineering methods" for design of software systems but then failing on the actual theory.

Another case was the M3 project [1,2] and now there's a group trying to replicate that work without even attempting to learn the underlying theory...go figure...

But as the paper goes on to state, verification is truly difficult - the size, internal relationships and complexity and interactions within a computer system is immense and very fragile. The paper notes a comparison between aircraft and computer systems; while an aircraft as complex as the Airbus A380 has as many "parts" as a typical large software installation, it can survive partial failure and, more importantly, we knew how the thing would behave mechanically before it even was built.

The discussion, and source of the second quote I'll take, then moved to the ethics and morality of using formal methods as best practice:

If formal methods is a best practice of software engineering, then an engineer who does not employ it is either negligent or incompetent. But formal methods is beyond the capability of typical software engineers (otherwise, why do we need formal methods experts and researchers?) or is too time-intensive to employ, so it cannot be considered to be a best practice today.

Sadly this quote is too true, but is deeply troubling when you consider how much software is actually in production.

I feel there is an irony here operating at many levels. After years of working with the UML - a language severely criticised by some for not being formal (and vice versa by others) and techniques such as MDA, we had developers using formal mechanisms without even really knowing it. Programming languages themselves are formal languages.

Then there's the irony of agile methods which apparently eschow any use for formality and modelling (so I am told and have experienced) - the irony here is that agile methods rely upon very strict communication between the developers, testing, validation, verification and common, consistent shared understanding of what is being developed.

Our own experiences of formal methods (Alloy, B-Method [4]) being used as a best practice have been documented [3] and the results we had very extremely encouraging. Though I do remember one episode where some "uber-architect" almost had a fit that we reduced his grand designs to a single page of relatively simple specification. I guess that simplicity was overrated - suffice to say, that particular design failed for many of the reasons given the the above paper.

Overall, the paper "When Formal Systems Kill..." is an extremely important discussion on software engineering failure to embrace and utilise the very techniques that it is based upon will some very damaging and frightening outcomes.

References:
  • [1] Oliver I, (2009) Information Spaces as a Basis for Personalising the Semantic Web. 11th International Conference on Enterprise Information Systems6 - 10, May 2009 Milan, Italy
  • [2] Oliver Ian, Honkola Jukka, Ziegler Jurgen (2008). “Dynamic, Localized Space Based Semantic Webs”. WWW/Internet 2008. Proceedings, p.426, IADIS Press, ISBN 978-972-8924-68-3
  • [3]Ian Oliver (2007). Experiences of Formal Methods in 'Conventional' Software and Systems Design. BCS FACS Christmas Workshop: Formal Methods in Industry, BCS London, UK, 17 December 2007.
  • [4] Ian Oliver (2006). A Demonstration of Specifying and Synthesising Hardware using B and Bluespec. Forum on Design Languages FDL'06

Friday, 25 November 2011

The Axiom of Choice and Mathematical Proof...(humour!)

Probably the most controversial axiom in mathematics, but quite simple really...as XKCD explains :-)



Proof by Intimidation needs to be added to the canonical list of "Proof by..."
Aside: an an undergrad many years ago I read a fascinating paper on reactive systems and after 3 or 4 pages of dense, complicated mathematics there was the statement: Proof left as exercise to reader.....it gives you some idea of the calibre of the author that he could get away with that (and no, I'm not telling who....)
anyway, a quick search using an popular search engine reveals a list which I'll just put a few choice examples:

Proof Techniques:

Proof by example
The author gives only the case n = 2 and suggests that it contains most of the ideas of the general proof.
Proof by intimidation
``Trivial'' or ``obvious.''
Proof by omission
``The reader may easily supply the details'', ``The other 253 cases are analogous''
Proof by obfuscation
A long plotless sequence of true and/or meaningless syntactically related statements.
Proof by personal communication
``Eight-dimensional colored cycle stripping is NP-complete [Karp, personal communication].''
Proof by reference to talk
``At the special NSA workshop on computer vision, Binford proved that SHGC's could be recognized in polynomial time.''
Proof by reference to inaccessible literature
The author cites a simple corollary of a theorem to be found in a privately circulated memoir of the Icelandic Philological Society, 1883. This works even better if the paper has never been translated from the original Icelandic.
Proof by flashy graphics
A moving sequence of shaded, 3D color models will convince anyone that your object recognition algorithm works. An SGI workstation is helpful here.
Proof by misleading or uninterpretable graphs
Almost any curve can be made to look like the desired result by suitable transformation of the variables and manipulation of the axis scales. Common in experimental work.
Proof by vigorous handwaving
Works well in a classroom, seminar, or workshop setting.
Proof by cumbersome notation
Best done with access to at least four alphabets, special symbols, and the newest release of LaTeX.
Proof by abstract nonsense
A version of proof by intimidation. The author uses terms or theorems from advanced mathematics which look impressive but are only tangentially related to the problem at hand. A few integrals here, a few exact sequences there, and who will know if you really had a proof?
Disproof by ``not invented here''
We have years of experience with this equipment at MIT and we have never observed that effect.
Proof by personal communication I remember as being something like:
"I met Knuth/Scott/Gödel/... in the corridor the other day and he thought it sounded ok"...

Note the the "Proof by Intimidation" above is slightly different to the XKCD example....both work....hmmm, might try this in my talk on the Theory of Privacy next week....did I tell you about that? Later....

I guess we could also add the "Proof by UML" from Software Engineering, this is explained in the excellent Death by UML [1]  paper.

Proof by Abstract Nonsense.....did someone mention category theory? ;-)


[1] Alex E. Bell. 2004. Death by UML Fever. Queue 2, 1 (March 2004), 72-80. DOI=10.1145/984458.984495 http://doi.acm.org/10.1145/984458.984495

Sunday, 20 March 2011

Fermat's Last Theorem

Currently residing on YouTube - possible the greatest documentary every made and a link to Simon Singh's superb book.

Part 1 is here:


and links to Part 2, Part 3, Part 4 and Part 5 .

Some more links:
And a link to the original papers.

Despite(!) the papers being presented in June 1993 and finally published in 1995, this still stands are probably one of the greatest pieces of mathematics every. Not much is going to top this in terms of breadth and depth - maybe proofs of P=NP (or not) or the continuum hypothesis?