Security Engineering Research Group

“Applications that Enforce System Security”

[These are comments to the paper titled, "From Trusted to Secure: Building and Executing Applications That Enforce System Security" available at USENIX ATC'07.]

The paper deals with the issue of differences between security enforcement on the operating system level and within applications. It describes a mechanism through which security labels of a MAC mechanism from the OS can be communicated to the application; the application provides assurance that it enforces the security policies within its logic; the output of information from the application is also communicated to the OS MAC mechanism to ensure that these outputs get the correct labels.

Things to notice:

• The architecture relies on security typed languages (Jif to be specific) to ensure that no illegal information flow can occur within the application
• The architecture provides an interface through which OS policies can be communicated to and from the application
• It provides a mechanism which provides assurance that the policies of the OS are being implemented correctly and
• It uses a high level policy to describe “declassifiers” — interfaces which are allowed to move information from high level of security to a lower level.

I found the last point of particular importance because it explained to me exactly what PRIMA meant by ‘interfaces which convert data of low integrity to high integrity’.

Another important point to note is that the information flow analysis to and from the application is not static (as in Jif - which uses compile time checks only, as far as I know) but dynamic in that the lattice of principals is created at runtime (meaning that mappings of labels to and from the OS would occur at runtime thus depending on the OS policy at runtime).

The developer does not have to know these mappings either. They are defined in a separate high-level policy so that they can be defined by the system administrator on the target machine.

The concept of mappings is particularly clarified through Figure 6 and the fifth paragraph in Section 4.3. The policy within the appplication allows pub -> siic -> sec. pub is mapped to security level s0 of the OS and sec to s1. Information can thus from from s0 to s1 (but only if this is allowed by the OS!) The Jif Runtime takes care of this sort of information flow.

Future directions of my interest:

1. policy compliance analysis between application policy and OS policy.
2. declassifier generalization (although the authors themselves have pointed out a few works in this direction).
3. issues of attestation of the architecture. (I believe this is not so straight forward due to the inter-linkages between different modules of the architecture but then, attestation is never easy anyway. )

Mental Slavery

The following link presents some philosophical jewels (novel approach) about study of mind and reality by professor shaz.

• http://shazkhan.wordpress.com/2007/12/18/mental-slavery/

I hope you like it.

Google Summer of Code

What is Google Summer of Code?

Google Summer of Code^TM is a program that offers student developers stipends to write code for various open source projects. Google will be working with a several open source, free software and technology-related groups to identify and fund several projects over a three month period. Historically, the program has brought together over 1,000 students with over 100 open source projects, to create hundreds of thousands of lines of code. The program, which kicked off in 2005, is now in its third year, following on from a very successful 2006.

While the majority of past student participants were enrolled in university Computer Science and Computer Engineering programs, GSoCers come from a wide variety of educational backgrounds, from computational biology to mining engineering. Many of our past participants had never participated in an open-source project before GSoC; others used the GSoC stipend as an opportunity to concentrate fully on their existing open source coding activities over the summer. Several of our 2005 students went on to become mentors in 2006.

Group Name/Domain

MMA has raised a good point which I would like to float here for discussion.

We’re currently calling ourselves “Security Engineering Group”. What if we move onto projects which are not directly related to Security. That would mean that our name is strictly restricted to security domain and we’re moving outside our domain. I agreed with MMA yesterday about this thing but I’ve had time to think about it overnight.

I am of the opinion that the name should remain unchanged for one reason: It will keep us focused. If we can get a project that is not related to security, our name will be a barrier in that case. But, the thing is that if we do not specialize in a domain, we can’t hope to get anywhere far with our research activities. Right now, we’re focusing only on security but are still having trouble addressing all fronts. We’re still in need of human resource. If we move onto more domains, it will make life more difficult for us.

So, my opinion. Keep the name, stick to the security domain.

This is open to discussion.

Some new selinux ideas

I have come across some talks about enabling selinux to achieve resource utilization using rbac. This sounds as a good research area. Do we have anyone to handle this.

Future Directions (and some extra stuff)

A.A. everyone.

Mr. MM: I was talking to Shahbaz yesterday and we talked about what research area I’m planning to pursue. I told him that I’ve been working with different sorts of things (web search etc) because I needed some publications. Now that I have some publications, I need to pick a single area and start working on that.

I have decided to pursue only Isabelle and the original goal of verification of security protocols. Of course, this is currently open to discussion but I talked to Mr. T yesterday too and he said he was very interested in the Needham Shroeder protocol verification given in Isabelle tutorial. I think I can cope with this protocol verification now and it would be better if I can get some hands-on experience.

Here’s what I think I’ll do. I’ll start with the protocol case study in the tutorial: NS protocol. Then, if that goes well, I’ll start with the verification of Kerberos V4 that’s available in AFP. That should be a complex enough case study and after that, we can hopefully start with some sort of verification of our own. Of course, in that I’ll need some expertise in the protocol side from one of you guys.

The reason for posting this here: First, the blog was getting too much like a news board and much less like a research blog. Secondly, I would like to take comments from you guys regarding (a) your interest in this research area of security protocol verification and (b) how you can contribute in this.

I plan on starting on NS protocol as soon as I finish writing the UML Spec paper inshallah. So, comments are expected and indeed welcome.

The Practical Part Starts Now

As soon as I am over with Recluze, I am going to start working with IPSec and SELinux now that my literature survey is complete (I think so). Next I plan to get some help from MR. MMA to let me in on his findings regarding how to stack IMA on SELinux.

I personally think using TPM’s PCR will be another good thing instead of IMA because IMA has more then I need. But according to Mr. MMA its very problematic. Sir have you tried to copy the technique IMA uses to address PCR.

Side by side I am trying to understand the functionality of the Tresys’ Policy Management Server and the module support it provides for policies because I am looking forward to incorporate it for ditributed MAC implementation.

One thing that confuses me, this is for Mr TAT and Mr. MMA, can we skip DAC if we use MAC? Is MAC’s use enough for OS requirements?

If we could just have a few more people we could start adjusting applications for MAC implementations! Its also a good idea for BSc/BCS projects. We could also move towards LDAP NIS etc.

My Blogg is working!

Its fresh and decent. Check it out?

Can anyone tell me how I can submit same posts to both the blogs mine and this one with one go? Hmm.

Verification introduction

A.A.

For the meeting of wednesday, here’s the agenda:

An introduction to Isabelle
An introduction to HOL
An introduction to Formal Verification Process

This is mostly for the benefit of Mr. T and for my own review.

I have the CSMR slides in binded form so those should be a big help.

Formal Varification Studies

AoA to the blog…
Rather replying on yahoo mail i preferred to continue on this blog as the benifits we all know :)… so Mr. MM is also interested in the combined study of formal verification so me and noman has decided to hav a meeting on Saturday morning… the timings will be posted on friday INSHALLAH… I am interested in more basic stuff first coz i dont hav previous knowledge of these verification type of things (all of us dont hav :)… so i ll inform masoom about the meeting and we ll hav the same voice conference over here in my office….

We went to Amin yesterday he has improved alot now and hopefully he ll join us in a month time INSHALLAH…

Noman is supposed to come to my office on wedensday morning to prepare the system for downloads and other archiving purposes… more after a break..

Take care.
AH