Security Engineering Research Group

Mathematical Skills

Mathematical skills are absolutely necessary for every researcher, who want excel in the research domain. An example can be taken of a PhD student, asked to specify its approach mathematically. Further steps, in this area means, not only specification, but some how, advanced steps, like verification.

Pakistan is currently short of such skillful people, and it is a our moral duty to practice such skills and propagate.

Though, its seems difficult now that how to manage our original research, together with formal or mathematical skills, but a pain in the start, is going to be a certain gain in the near future.

Isabelle/HOL Tutorial

Isabelle/HOL tutorial download link, especially for Mr. T:

http://www4.in.tum.de/~nipkow/LNCS2283/tutorial.pdf

See chapter 10 for Needham Shroeder Protocol case study.

HOL-OCL Installation Instructions Posted

Instructions posted on:

http://recluze.wordpress.com/2007/06/17/installing-and-configuring-hol-ocl/

Thoughts on Z

I’ve worked with Z notation now for a complete specification and here are my thoughts regarding the experience.

1. Now I know why Z is losing clientelle and why software engineers are reluctant to use it in practical scenarios. It has all the problems normally associated with structural programming approach and none of the benefits. It also has all the drawbacks of formal methods and almost none of their benefits.
2. It’s difficult to organize your thoughts when you’re working with a large enough specification. I saw this in the Usage Rights Document and I’ve seen it in my own work. The individual parts are easier to understand and keep track of but it’s much more difficult to keep the big picture in sight. 
3. In my opinion, the semi-formal methods (such as UML+OCL approach) or the purely formal methods (such as those supported by Isabelle) are a much better way to go. I have seen the theory HOL-OCL (along with the complete architecture) developed by the guys at ETH, Zurich and I like that approach. It is a more streamlined approach and one that is more likely to be accepted by the industry. I’m not the only one to think along these lines either. The introductory parts of the HOL-OCL book describe why exactly Z has never gained support from the industry and why UML+OCL have succeeded in doing so.

I’ve started working on HOL-OCL and I’ll be reporting my findings and thoughts related to this approach. I know this is yet another shift in direction for me but I believe it’s necessary to try all options and then stick to one. These are just tools and my experience with each passing tool has taught me that the glue in all these formal methods nowadays is Isabelle.

[Mirror post on http://recluze.wordpress.com]

Zeta + HOL-Z presentation

A.A.

I’ve uploaded the second presentation regarding ZETA and HOL-Z: Take a look.

Update on Z

A.A. everyone (whoever’s left here)

I’ve almost finished the specification part of the OSL. (That’s chapter 2 in the DoCoMo document.) I’ve also created a complete (albeit simple) specification in Z and type checked it using ZETA. I’ll be uploading that pretty soon inshallah. I feel pretty comfortable with Z.

I would like it very much if Mr. MM can update me on roughly what portion of the Usage Control he’s working on. I know it has something to do with his SECTET and the higher level abstraction but I’m not sure. If it’s not suitable to be put in public writing, a mail would also do.

Secondly, I would like to know what I’m expected to contribute in this area? I have a few ideas but most of them are half-baked as of now.

ZETA Presentation Uploaded

Please take a look:
http://recluze.wordpress.com/2007/04/27/zeta-presentation/

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.