Security Engineering Research Group

The Page Can Be Visited!

AOA all guys

Shaz the jazz guy… The link can be easily copied …. no worries. Ok guys wats up howz is Masoom sb and Tamleek sb! i couldnt talk to them for more than a month or so… wat ever… my salam to both of them…and wish them a good health.

tc
bye.
amin.

Specification/Verification in Isabelle Finally Starting

Alright. After much waiting and detours, I’ve finally decided to start doing some original work in Isabelle/HOL itself. *drum rolls*

After the last meeting with Mr. MM, I’ve decided to start working on the specification I’ve already done in Z of his framework. The specification is pretty involved and would require much more work to be properly embedded in HOL. I have a few ideas but that will have to wait.

Mr. MM: Here’s my plan. First of all, what needs to be done is that we need to have the Document Model formalized, specified and verified. This has already been done during HOL-OCL development by the ETH Zurich guys but I would like to do it in a more accessible way (i.e. without the use of stuff like “smashed sets and objects”). I want to make something that can be used by the average formal specification engineer. If we can get only this done, it would be an accomplishment.

So, I would appreciate it if you can take some time out and find out for me if the Class Diagrams of UML have been formalized in Isabelle/HOL. I’ve done thorough searching and have only found stuff done in either HOL-Z or HOL-OCL (all by the ETH guys). I want to make sure that I’m not re-inventing the wheel. I’ll continue my search but it would be a big help if you can confirm that it has not been done before or find me the papers which have done it.

SVN Error on PMS Checkout

Shaz: I haven’t been able to download the PMS through svn. I get this error:

svn: PROPFIND request failed on ‘/home/repos/policy-server/branches/selinux-pms-support’
svn: PROPFIND of ‘/home/repos/policy-server/branches/selinux-pms-support’: 405 Method Not Allowed (http://oss.tresys.com)

HOL-OCL Installation Instructions Posted

Instructions posted on:

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

Some How..Am Back!

AOA all guys

I am back with my 200/- rs. card in my cdma system which is halfway over…. nevertheless i thought to have an email contact with you all guys. i hope all of u will enjoying good and sound health. same is here.
Eventually i found a page which i thought…could be good for u guys and not a great deal for me as am out of the race since more than 3 months. still give a look to it.
here goes the link.

http://virt.kernelnewbies.org/TechComparison

Meeting time this Friday

Salam every one,

I have talked to Tamleek sb, and he agreed with me that if meeting time can be moved to evening such as 8 or 9 PM in Pakistan. The reason is that we can then talk very flexibly and till longer duration. Nauman please comment on your availability on Friday evening.

Blog Stats

A.A. everyone,

In case you guys haven’t seen it yet, here’s a link for our blog statistics. It shows page hits etc. It also shows what search keywords people use who reach our blog. It’s useful if you’re trying to see what audience you’re receiving.

http://securityengineering.wordpress.com/wp-admin/index.php?page=stats

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]

Need a Book

I had an email correspondence with Trent Jaeger who made labeled IPSec. He suggested the following book for Trusted computing related questions.

   o Sean Smith’s book on Trusted Computing Platforms.

Mr. TAT can u get it for me from that website? Or somewhere else?

He also said that consistent policies which are necessary for distributed MAC can be achieved via a hiher level service which distributes policies. This mean my direction is just the right one. I hope we get it over in time!

Where is Amin saib?

For Nauman

http://eprints.eemcs.utwente.nl/6945/01/TR-CTIT-06-62.pdf

Take a look at this.

Best,
MM Alam