[cap-talk] Formalism in computer security discussions

[Toby Murray]

Jed at Webstart wrote:

> At 07:33 PM 5/23/2006, Toby Murray wrote:
>
>> Hi cap-talk,
>>
>> A question for anyone more familiar with modelling security properties.
>> I'm currently working through a paper "Multilevel Security and Quality
>> of Protection" that looks at reasoning about multilevel secure systems
>> in terms of quality of protection.
>
>
> Hi Toby.  I assume this is the paper you're looking at:
>
> http://www.cs.ucc.ie/~simon/pubs/qop2005.pdf 
> <http://www.cs.ucc.ie/%7Esimon/pubs/qop2005.pdf>
>
> ?  I often find it confusing to get multiple layers of filtering
> about what's being said in a paper.

Yep, that's it.

>
> I read a bit of this paper.  One comment I feel compelled to make is to
> ask people on this list how they feel about such mathematical formalism
> in discussions of issues like multilevel security.  While I do have 
> sufficient
> mathematical background (Masters in Math that of course included
> set theory and abstract algebra - mostly what they use in this paper),

I don't have a very strong maths background and tend to have to force 
myself through the formal parts anyway, often with limited success :)

> I find it, well, tiring to follow though sections like the last three 
> paragraphs
> in section 5 in that paper, e.g.:
>
> The classical Constraint Satisfaction Problem (CSP) is a Soft CSP (SCSP)
> where the chosen c-semiring is: S CSP = <{ false, true}, v, ^, false, 
> true>.
>
I also had trouble understanding this. I don't think there's enough 
detail in the paper about semirings (or c-semirings) to figure out 
what's going on with them. If I get time I'll read their previous paper 
that specifically deals with them and then see whether I can make more 
sense of this paper.

> While I've struggled through such formalisms many times, I have to admit
> to be disappointed to never (really) finding any additional value in doing
> so.  I'd be interested to hear the experience of others in this regard.

To me, I'm not necessarily sure that the formalism is completely useless 
if it doesn't help one's understanding. On the other hand, if someone 
like you can say "yeah, I can reasonably see that this formalism 
accurately models the real system" and then if useful results can be 
obtained from using the formalism to model real systems, then isn't that 
a win?
In particular, I find the SCOLLAR work illustrative here. I'm still yet 
to wrap my head around their formalism -- particular the proofs about 
safety being decidable etc. (which I think appear in an appendix to one 
of the relevant papers although it's been a while since I've looked at 
these papers). But the work does clearly demonstrate restrictions that 
must be followed by various parties using the Caretaker pattern, for 
example. These restrictions hadn't been enumerated before in the 
literature (I don't think). Having an exhaustive list of conditions 
under which the Caretaker breaks is useful, no? It helps our 
understanding of this pattern better. Plus which, their results are 
fairly easy to map back into the "real world" (eg. E) so that ordinary 
programmers (such as myself) can make sense of them, I think.

> One of my first big disappointments in this area was the Bell and
> LaPadula model.  When I first saw one of their papers I thought to
> myself, "Oh boy, now I can really put some of this formal training
> to work and use it to get a better understanding of computer security"
> <where I was doing research at the time - middle 1970s>.  Sadly
> I found that from my perspective the formalism simply served to
> obscure what was really going on and to exclude many people from
> being involved in the discussion - thereby giving the illusion of greater
> substance to a model that was and is, in my opinion, fundamentally
> flawed.
>
> I'd be interested to hear the reaction of others to such formalism
> when they've encountered it.  Has anyone ever had a positive experience
> in this area?  Namely an experience of wading through (or perhaps being
> delighted by) the formalism in such a paper and finding that it really
> contributed to their understanding of the basic concepts?  In that
> case I would like to read such a paper and perhaps get reenergized
> in this area.  If not then perhaps people can express opinions on
> why such formalisms are as common as they are.
>
I find the idea of being able to prove that a capability abstraction 
(such as the Caretaker or whatever) can enforce certain security 
properties in a system. If Alice can be mathematically certain that her 
pattern (like the Caretaker) enforces the policy she's interested in 
having enforced, no matter what the other entities (that she doesn't 
trust) in the system might do, then to me, that might be really useful.

-- 
Toby Murray
Advanced Computer Capabilities Group
Information Networks Division
DSTO, Australia

IMPORTANT: This e-mail remains the property of the Australian Defence
Organisation and is subject to the jurisdiction of section 70 of the
Crimes Act 1914. If you have received this e-mail in error, you are
requested to contact the sender and delete the e-mail.