Security Engineering Research Group

Linux Kernel Programming for Newbies

I have been wondering lately how we can develop a team of coders — expert coders — who can take our architecture and idea designs and implement it! The problem is, I have never worked on the kernel code. I would like to start a single post here in which we can get an outline of how a newbie can start with Linux kernel programming. I would like guidelines about:

• Any books which can be followed

• The flow of how a newbie (with C/C++) experience can embark upon learning kernel programming
• Tips (like the LXR) etc

Blog Change

I just saw the new interface of the blog, it seems ok but i cant find the “HOME” that i normally had on the blog page. Can you put that on the page or having another interface having Home tag in place.
Thanx

Security Engineering on Isabelle World Map

Now, the world can know that we’re working with Isabelle. Check out Isabelle’s world map here. And Tobias Nipkow was here in Peshawar! In March. When I was working my head off trying to get to grips with Isabelle. That was a chance missed.

Protocol Nonce Question

I have a question and I was wondering if one of you security gurus can answer it.

There’s a lemma in the “Message” theory in Isabelle. It says, “In any message, there is an upper bound N on its greatest Nonce”.

In Isabelle:

lemma “Ex N. !!n. N <=n –> Nonce n ~: parts {msg}”

The lemma, translated to English says, “There exists an N such that for all Nonces, if N is less than the nonce, this greater Nonce is not in the message” or “there is a Nonce of number n which is not in the message”.

Can somebody shed some light on why this might be so? Or why we’re bothering with proving this?

Note: Isabelle protocol verification theory does not give any motivation for the lemmas it’s proving. It’s just going about merrily proving all sort of seemingly repetitive theorems.

Needs of network for MAC

After the comparison of trendy MAC enhancements, I have been figuring out the general needs of a network for MAC. We have three places where MAC can and is enforced:

1. In Application: Where flow control of application is controled by labeling the data of the application. Current research is limited to MLS becuase its simple. And because the security type languages are not mature enough to handle the granularity. I have seen two framworks at this level, which make use of these languages. One of them has been partially integerated with selinux by using the application layer API to selinuxfs. I am curious why they are so interested in JAVA! There is no C extension.
2. On Application Layer: This is achieved for applications that do not use TCP/IP directly. They use RPCs so the common network controls cannot handle properly. The reason is that port to application mapping is done by portmapper daemon. Thus the rpc headers carry the security contexts. Such applications are NFS and NIS.
3. At TCP/IP Layer: Here the ports are labeled for the associated applications on both sides. I a hostile environment this would not prove useful so encryption would also be required. This is achieved by IPSEC associations being labeled. I am not fully satisfied by the mechanisms at this level because at one extreme we have lack of security and on the other hand manageability issues.

LDAP is on the todo list but nothing is currently being done about it upto my knowledge. The todo list also wants more granularity and API at TCP/IP layer.

Policy distribution being a great issue has no solid solutions yet. The only possibility to till now is a tranlation server, which would provide an equivalence mehanism for internode security contexts. But this is has been left as an idea and no progress is being made. IPSEC associations were provided only for subjects but currently they are working for providing object support but the work is hidden yet. They are thinking for CIFS support as well. Ephimeral ports can be handled with standard SELinux API for applications.

The biggest problem with distributed policy is the type enforcement, which is part of the security model/context. Leaving it out would be a solution but will affect greatly because code bindings will be lost, which will result in loss of integrity control. The context has three main models. User identity, role and TE. If one is lost it will affect the others because they are tied together to help each other. I am figuring out how much affect will be made. At the same time integrity can be measured with IMA and alike. I would like comments on what you ppl think about the differences in the integrity model of TE and IMA.

If anyone can come up with other ideas of network needs plz brainstorm so I figure out the requirements. There are others which I have’nt mentioned because they are trusted applications by SELinux. I find a gap over here because trusting applications is not a good idea. Information flows can work here. More on this when I get a solid insight on them.

What do you guys think should be my next target. Amin is sorting out to integerate his study with all this. So give ideas of possibilities. Any of you who thinks their work can have relevance plz share your findings so that we can be more useful to each other.

Install Windows Vista in a Mac OS X environment using VMware Fusion

It is indeed possible to run both Microsoft Windows and Mac OS X at the same time on a single personal computer. The key is VMware Fusion, a virtualization platform that allows you to run Windows in an OS X environment. This How do I… shows you how to install Windows Vista in an OS X environment. If you currently own an Intel Mac and want to run Windows alongside OS X, this tutorial is for you.

 http://ct.techrepublic.com.com/clicks?t=39742567-a4acee59e60b2ede1d9ae2fca3986a14-bf&s=5&fs=0

amin.

Protocol Verification in Isabelle

I’ve started working with the development of framework for protocol verification part of my Isabelle related work. Currently, this is simply copying of the Messages, Events and Public-key portion provided with Isabelle. This is mostly for my understanding. It’s already developed and many helpful theorems are already proven. They can be used as-is but that would mean a lot of efforts during our own proofs.

I’ll be posting my progress (in the form of regularly created PDF) here as it’s already publicly available on the internet: It’s mostly to show anyone interested what my progress/status is.

Download the PDF here.

4th International Conference on Innovations in Information Technology–Review

Submission

Innovations’2007 seeks original full-length (5 pages maximum) paper proposals describing research in all areas of Information Technology that contribute to the conference theme. All papers will be peer reviewed. Acceptance will be passed on quality, relevance and originality. Accepted papers will be published by IEEE and fully indexed in IEEEXplore. Proposals for tutorials and special sessions are also welcome. The submission guidelines can be found on the conference web site:

http://www.it-innovations.ae

Conference Journals

Selected papers of the conference will be considered for the following International Journals:

- Journal of Communications, Academics Publishers,

- International Journal of Web Services Practices, Computer Science Press,

- International Journal of Information Technology and Web Engineering,

Idea Group Publishing
Important Dates

Papers submissions deadline extended: August 28, 2007

Notification of acceptance: September 22, 2007

Final camera ready papers due: October 27, 2007

I would like all members to give any comments regarding this conference….

amin.

Updates on Research and Other Status

A.A. once again every one!

After a long time, I have regained my ‘dil ka zore’. I’ve  been through it before — many times. So, I’m pretty used to it by now. It’s always left me with a lot more knowledge than I would’ve gained without it.

Anyway, I think I have a job in City. I have an office at least. I have setup my FC6 and Isabelle (once again) and have started working on the Message formalization for security protocol verification.

Once again, I would like to invite all of you to start working to make this group better. I know we’re all very busy with what we do. But this group is a commitment and I’m sure you all appreciate that there aren’t many people in Peshawar who can work on research the way we are currently working. If we want to continue with our work (which is taking a pretty good shape, btw), we need to work together and not through some disconnected communication in email.

I’m especially expecting a lot from Mr. MM and Mr. T. You two are the leaders and being that you have to provide with the sacrifices. Iss dafa qurbani ka baqra aap loge khareedain gay aur group ki taraf se qurbani kerain gay.

As for my part. I’m just waiting for my internet connection and then I can start the voice chat with Mr. MM regarding Isabelle. Shaz has said more than once about Calculus but I’m not sure that was serious. Anyway, I’m ready for that too and Lisp is always easy — if someone needs it.

Now, I expect to see some comments here. Get writing!

Eclipse, Java, C++, Lisp, LaTeX and Isabelle

New post (after a long time) on my site. If you’re interested in either Eclipse, Lisp, C++, Java or LaTeX, you need to see this:

http://recluze.wordpress.com/2007/08/17/eclipse-java-c-lisp-latex-and-isabelle/