JTurret

About

JTurret is a security contract WatchDog. It enforces "Design by Contract", a concept introduced and popularized by Bertrand Meyer. Design by Contract, or DBC for short, outlines expectations of computer software and verifies if the software correctly satisfies the expectations. The specification of the expectations is supplied through a contract, either during the process of implementing computer software or later, for a verification of behavioural characteristics of the computer software.

JTurret, principally, is designed as a verifier and hence it is more appropriately tagged as a Watchdog.

Contracts

As discussed above, the specification of behavioral requirements are supplied through a contract. Before, we outline how contracts can be specified, it is more fitting to supply a small example.

Consider the case of a regular LIFO stack. In the usual case, the stack is defined by a specific size. For a better understanding of bounded stacks, refer Paul Black's primer. The computer software should never insert an element onto the top of the stack if the number of elements in the stack already equals its size. A failure to adhere to this crucial precondition, can be extremely dangerous.

Although this example is considerably simple, it still identifies an approach to the specification of behavioural characteristics. Meyer, thus identifies three important meta obligations that can be used to define contracts:

Pre-conditions: expectations to be satisfied prior to an invoke.
Post-conditions: expectations to be satisfied before returning control.
Invariants: expectations that must be maintained throughout the execution of the program.

Each of the above, individually present a few issues in how implementation can be and has been carried out. I have made an effort to address all issues in my paper (here (pdf)).

If the idea interests you more, please consider:

Meyer's original paper (can be downloaded off the net).
A description of the EIFFEL site.
The other softwares I link in my paper.

JTurret allows contracts to be specified using linear temporal operators. Linear temporal operators are logical operators that model time, in a sense. What is interesting is it allows to consider Preconditions and Postcondtions as states that "must" be reached from the current state. Or rather, we can move from State 1 to State 2 only if the conditions, as specified, are satisfied (Precondition). We can then stress that we could move from State 2 to State 3 (if state 2 is assumed to be the invoked module), only if a subsequent condition is satisfied (PostCondition).

Downloading JTurret also includes many examples on how contracts should be specified, the API docs, and almost all the necessary tools.

I evaluate Precondtions (Past Linear temporal logic) by a recursive technique I had studied from a Security thesis ( Refer to the bib).

I evaluate Postconditions (Future Linear temporal Logic) by first converting the same to a generalized Buechi Automata and evaluating this at run time. While this might not be the best technique, it certainly helps to work with a the issues that arise with temporal operators.

I also discuss, and have implemented, a few alternatives. But they are more to serve as references as opposed to be them being actually used.

The JTurret places itself in the JVM and as the client software or Programs run, the execution is constantly monitored. If for instance, com.foo.FooClass is loaded into the memory, and com.foo.FooClass is also specified in the contract to meet with some post conditions, JTurret guarentees this is satisfied. Failure to do so, raises an exception. The exception can either be logged, or made to quit (the safer option).

Paper

The supporting paper can either be downloaded from the Downloads section or the latest version can be got from my website.

Developer

Vaishak Belle (write to me if you are interested to work on/extend).
If there are any updates, I usually post it on my website: http://www.meltonfoundation.org/vbelle/

Disclaimer

This Software is supplied as is and does not come with any warranty. For license details, please check the appropriate section on the sourceforge page.
Due to time constraints, I couldn't complete the tool as I would have liked. While, I believe most of the code throws sufficient light into the actual techniques, it might not run as smoothly as I desire. If you have any feedback, please drop me a line.