Security Engineering Research Group

Tamleek sb ‘wadaaa’ pa Khusay kay!

What about this?

Re: Update and Questions

Salam All,

Kindly find the link below. Kindly let me know about your availability about a discussion on case studies about Z notation and all that. I will also suggest, that if you can prepare some slides regarding on “How to Hol-z at work”, then, we all can start a combine effort to master this tool, like you can start on one part and i can start the other part.

You have already posted some instructions regarding Hol-z, but i will recommend to make a more slide view for us. Is this possible for you to meet on this Saturday? late evening some time or ….
http://www.docomoeurolabs.de/pdf/publications/2006/2006_STL_Enforcement_for_Usage_Control_System.pdfBest,
MA

AA
Nice work noman… i m really happy with the efforts you put so far in this area… Printing the book is not a problem i can arrange things from ims otherwise i ll buy RIM for you and you can get it printed over here… binding apnay paisoan ki ;-)….

For MM i ll suggest that he should now give that Z-specification of the shneider from Germany… i know m wrong  in his name :-)… or any other material regarding “usage control”… so that nouman can start working on that or atleast understanding it…

And on my part i hav finished with the invitations to my relatives… i know you all will also be waiting for your cards… but m not gona give cards to any of you (coz of its shortage) you all are invited on Valima on 6th May for lunch… i wont mind to hav gifts from any of you… specially MM can send gift from there as well… shipping wont cost much (i hope)… You all are requested for prayers…

Mr. T

Update and Questions

A.A. everyone.

Nothing going on in the group scene? Isn’t anybody doing anything? Or should I say, isn’t anybody writing anything about what they’re doing?

Here’s my update on my work with Z.

I’ve almost finished the Using Z book. I’m on to the chapter that has the first case study - the file system. This book not only has the specification part of Z but also the analysis/verification part. Very good book, not only for learning but also as a reference.

I’ve also covered the Birthday Book example that comes with all tools of Z. I’ve seen how HOL-Z takes Z notation specification and performs verification on it. I’ve done practicle upto the point where one generates .holz file. I’ve yet to load it in Isabelle and actually perform the verification.

I believe I need two things now:

1. The Using Z book needs to be printed. It’s great to be kept as reference. Since I’ve covered a whole semester’s worth of notes in a week, it keeps sliping out of my mind. I need some sort of printed material next to me so that I can keep reading it whenever I get a minute free. Unfortunately, this is outside my resources as the book is 409 pages long. It would be really nice if “someone” (I dunno, probably someone who’s in ims’s faculty can get it printed. I only need it for a month or two. It can go back to IMS as a reference book or something. Is it possible?
2. Like Mr. T said in the last meeting, it would be really nice to have the base work that Mr. MM is working on. Now, I can understand Z almost completely and it would be really nice to be able to practice on the targetted area alongside the textbook case studies. I’m continuing with the book case studies but it would be better (and less time consuming) to also start work on the targetted specification. Mr. MM?

I have paper going on currently, so I can’t give full time. I’ll be free by 28th of this month inshaallah. I’m really hoping we can get some sort of publication in verification area.

Novell…Securing Linux Systems Wuth AppArmor

AOA

i just lookin at this stuff…. its really good and vastly supported by novell..here is the link.. a detailed pdf is also there..have go on this link.

AppArmor Linux Application Security: Overview:

tc
bye
amin.

AppArmor

Shaz: Quite hot discussion going on this software. I dont know, but seems to me that it is some thing parallel to SElinux. study it and tell us, as you are working on SELinux, it will nice, if you also see the accompanying technologies.

Best,
MA

Nauman: Tomorrow Meeting?

InshAllah, we will meet tomorrow on friday.

Best,
MA

For shahbaz

Kindly check for my comments on your blog.

For all: It will be a good practice to write comments on each respective blog, rather than creating new entries. The outlook  is cool.

Best,
MA

Interruption?

Actually, I like it more this way. I think the blue/clean theme looks better. Just leave it as it is. Or ask others about it.

Installing HOLZ

A.A.

I’ve written a small tutorial for installation of HOLZ with Zeta. Read it here if you have trouble installing HOLZ.

Secondly, I’ve finished the 7th session. From Mr. MM.: You said you’ve been working with Z. I need to know how you actually work with Z. I’m talking about tools used. Do you do it using pen/paper or do you use a tool? I’m asking because here’s how HOLZ works:

The actual Z notation is written using Latex! (I knew my efforts with Latex wouldn’t go in vain.) The latex source is converted to PDF by Zeta. (Or to HOLZ if you install the adapter.) This HOLZ file can then be loaded into Isabelle/HOLZ and theorem proving can be done there. So, if you know how to encode Z notation in latex, you get a head start. If you know latex, that shouldn’t be much trouble. Otherwise, some work will need to be done on that front too.

This is one question I’d like an answer to before the next meeting.