Security Engineering Research Group

My Status on Conferences

A.A. everyone,

I’m leaving for Karachi today (after about one hour). I will know today whether I’m going to Ireland or not. If I get a visa today, I’ll go there. If I don’t, I’ll come back to Peshawar and go to Karachi for the Khi Conference on the 5th.

So, if you need me for anything, well, you can’t find me Shaz: Please reply to my mail regarding prayer timings as soon as possible.

Mr. MM: I’ve submitted the abstract to ICET2007 in the form that you last sent me. (I’ve changed spec eng. to software eng.)

And Amin and Mr. T: Please don’t delay the abstract. Please remember that we’re trying to make submissions as a group, so, we need everyone’s submission to reach that conference!

Kindly pray for me, everyone.

IMA info required

Salams, today we had a comprehensive talk about selinux, trusted computing and formal methods. It was a good get together and we need to have these on regular bases.

Secondly, Mr. MMA discussed his experiance related to IMA usage side by side with selinux. He will share his experiance with us. This will benefit me and Mr. TAT.

I am expecting the code snippets and know how of the process that Mr. MMA used on this blog or on our mailing group. This is required soon!

Thirdly, we can utilize this blog for a lot of communication. I request group members to post their updates regarding their specific topic and this will benefit all of us. Apart from this we can share other things off the topic that we come across for knowledge sharing. If someone is feeling shy regarding their ideas that they might be stolen, we have our mailing group which is always there! This keeps everyone motivated and it makes the tough gets going if u understand what I mean. It promotes the competitive psyche and everyone will work hard then.

Core 7

Congradulations! Fedora Core 7  has been released.

Mr. TAT plz put it on download tomorow. I have some other things to download too. Maybe I’ll show up tomorow.

Pussy cat and the babies Shit!

Yes thats true Mr. TAT’s office is full of cat shit and it smells very bad so we did not do any study today at his office. Asghar kaka was asked to remove the cats so that humans can continue to rule.

Tomorow at 07:30 am our session is decided and I hope everyone shows up on time including me!

We are going to have a TPM emulator presentation from Mr. TAT. An IMA presentation from me. And we are also going to discuss recluze’s paper on folksonomy which has been accepted in karachi for some conference.

We hope to communicate with Mr. MMA as well regarding something I don’t remember now. I hope the electricity is there and that the internet bandwith is fine. Tomorow is holiday so we are going to have good bandwidth if Mr. Nawaz is not downloading videos.

Progress

Today we installed a linux fc6 machine at Mr. T’s office. It is configured both for experiments and study/research/publishing requirements. Recluze promised to automate all the configuration steps because using the same machine for both purposes was not a good idea but as we are always in a aweak position so we had to cope with it. The system is expected to crash and/or get dirty with experimental work. He has been working fancy with it so I am not aware totally what the system has and how he’ll automate the configurations. We would like your comments with some explaination recluze.

We will start with tpm emulator and ima setup tomorow if Mr. T shows up. I have’nt called him yet. Later we will see if I can also adjust my selinux interfacing on the same system but I doubt it. I hope Mr. T can get me a system also. Mr. MMA sir can you let me have details regarding your findings regarding the interfacing of selinux and ima?

I am writing up the abstract that you asked for and in June there is an IEEE conference exactly with the same requirements so the time constraints and my interests fit in properly.

A trip to village

I am leaving for my village tomorow. LXR is at the moment stuck at cgi and apache problem. Apache picks up lxr stuff but does not process the cgi scripts rather prints it as html!

I’ll see to it after I come back on wednessday. I am also planning to start working on my thesis. I cannot take more pressure because I have to start earning. Our family ppl do not understand and do not want to understand what I want to and I think they are right.

And who says that research can’t be done with jobs. They rather get a bit slow. Not good for a competitve environment but hey I’ve got Allah on my side. But who said we’ll be doing research only and no jobs!

Any good ideas where I should apply? I would prefer Peshawar university. Have good links as well but how do I apply and what for? Plz help needed!

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.

Z continued…

Thanks sir (Mr. T),

The book shouldn’t require a whole rim. It should take 205 pages only as we need to print on both sides. Binding isn’t a problem. Secondly, I’ve downloaded the file Mr. MM’s talked about. I’ll get that one printed myself. We should work on that. I’ll start working on the HOLZ presentation ASAP.

So, when will you be free so that I can come to IMS for that RAM and for this stuff?

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.

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.