Spinroot

A forum for Spin users

You are not logged in.

#1 2012-08-30 12:18:45

Mirza
Member
Registered: 2012-08-30
Posts: 6

Verify security properties using model checking technique in Promela

The flow is considered secure if it accepts a specified policy. Trying to develop a conditional transition system which is able to preserve the security properties and prevent unauthorised information flow to flow from one process to another.

For eg;
assign security levels to subjects(A Manager) and objects(A file). All the subjects and objects are labelled for confidential , public. {A manager is trying to access a file}

so he must satisfy the condition that he has the level of authority to access the file , if the manager level is equal to or higher than the object he should be allowed, but if clerk tries to access the file he should be rejected

Aim is to show allowed flows and rejected flows AND VERIFY SECURITY PROPERTIES

I have done a case study of E-commerce system with all information flow 

   
chan EPay2Store = [0] of {mtype, byte};
chan Client2EPay = [0] of {mtype, byte};
chan Client2Store = [0] of {mtype, byte};
chan Bank2EPay = [0] of {mtype, byte};
chan Store2Provider = [0] of {mtype, byte};
chan EPay2Client = [0] of {mtype, byte};
chan Provider2Store = [0] of {mtype, byte};
chan Store2Client = [0] of {mtype, byte};
chan Store2EPay = [0] of {mtype, byte};
chan EPay2Bank = [0] of {mtype, byte};

/*All processes involved in the case*/
proctype EPay()
/* define subject (S1) and objects of cloud Lattice C0*/
{
    Store2EPay ? AskPayment(_);
    EPay2Client ! MakePaymentRequest(1);
    Client2EPay ? PayInformation(_);
    EPay2Bank ! RequestPay(1);
    Bank2EPay ? ConfirmedPayment(_);
    atomic {
        EPay2Client ! Receipt(1);
        EPay2Store ! InformStore(1);
    }
}
proctype Store()
/* define subject (S2) and objects (O2, O3) of cloud LatticeC1*/
{
    Client2Store ? BuyRequest(_);
    Store2Provider ! Check(1);
    Provider2Store ? Confirm(_);
    Store2Client ! Replay(1);
    Client2Store ? xxx(_);
    Store2EPay ! AskPayment(1);
    EPay2Store ? InformStore(_);
    Store2Provider ! InformProvider(1);
}
proctype Bank() {
    EPay2Bank ? RequestPay(_);
    Bank2EPay ! ConfirmedPayment(1);
}
proctype Provider() {
    Store2Provider ? Check(_);
    Provider2Store ! Confirm(1);
    Store2Provider ? InformProvider(_);
}

proctype Client() {
    Client2Store ! BuyRequest(1);
    Store2Client ? Replay(_);
    Client2Store ! xxx(1);
    EPay2Client ? MakePaymentRequest(_);
    Client2EPay ! PayInformation(1);
    EPay2Client ? Receipt(_);
}

init {
    atomic {
        run EPay();
        run Store();
        run Bank();
        run Provider();
        run Client();
    }
}>`


****I have to give levels to the msgs so that the model checker checks the conditions and decide to give error and reject the flow OR  let the message to flow ****

**I'm having trouble to put the conditions in between** I hope you got the issue its using the formal model checking technique to validate security properties of a system .

Many Thanks in advance for the support

Offline

#2 2012-08-30 12:33:06

Mirza
Member
Registered: 2012-08-30
Posts: 6

Re: Verify security properties using model checking technique in Promela

Please show some light on the issue and suggest how it can be done.I want to give levels to the msgs and check condition ... how is that possible ???

Offline

#3 2012-08-30 19:29:14

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Verify security properties using model checking technique in Promela

I am not sure what your are asking?
Messages can consist of multiple fields.
You can check conditions with if-fi constructs, or with assertions, where appropriate.

Offline

#4 2012-08-31 07:25:59

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Verify security properties using model checking technique in Promela

Mirza, what is the level of msgs? Do you mean the priority of the msgs? High priority msgs are sent and received before low priority ones? If my guess is right, you may consider "sorted send" (!!) and/or "random receive" (??) statements of channels.

Offline

#5 2012-08-31 14:54:41

Mirza
Member
Registered: 2012-08-30
Posts: 6

Re: Verify security properties using model checking technique in Promela

for example when I would sens a msg from process A which is at level 0(L0)to process B which is at level 1(l1) the msg should be allowed to flow from the channel according to write up is allowed , but msg frm l1 to lo it should given an error as it violates the security policy. ....
I hope you got it.

Can you give an example how to use multiple fields and put condition to check the level of msg.

Thanks very much guys...

Offline

#6 2012-09-04 12:20:16

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Verify security properties using model checking technique in Promela

For example, multiple processes share a channel called com_chan.

chan com_chan = [1] of {byte, ... } /* The first element symbolizes the level */

proctype process(byte proc_level)   /* proc_level indicates the level of the process */
{
    byte msg_level;                      /* A local variable to receive the level of the msg */
   
    if
    :: com_chan ! proc_level, ...      /* Send */
    :: com_chan ? msg_level , ... ;   /* Receive */
        if
        :: msg_level > proc_level ->   /* If the level of msg is higher than the level of process */
            assert(false)                    /* Flag an error */
        :: else                               /*Normal operation*/
        fi
    fi
}

Offline

#7 2012-09-08 17:00:18

Mirza
Member
Registered: 2012-08-30
Posts: 6

Re: Verify security properties using model checking technique in Promela

thanks feng lei 76
the main motive is to implement a security property
No READ UP (A LOWER LEVEL CANNOT READ HIGHER LEVEL)
NO WRITE DOWN(A HIGHER LEVEL CANNOT WRITE TO LOWER LEVEL)

Is it possible to have read and write operation and define security ???

I have tried this it working, and was of great help?? as I'm new to promela

Offline

#8 2012-09-09 22:12:38

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Verify security properties using model checking technique in Promela

I think you're asking us to design the protocol for you.
What spin can only do is, though, to check *your* designs, and once you have one, we can help you either to specify it and/or to check it, depending on where you get stuck...

Offline

#9 2012-09-13 22:27:11

Mirza
Member
Registered: 2012-08-30
Posts: 6

Re: Verify security properties using model checking technique in Promela

I'm just trying to implement what you suggested. I'm getting an error which I have written below , I tried to Google it but didn't find any description.  could you just tell me where am I going wrong in the code It would be of great help as I'm  stuck in the initial verification.

spin: line   3 "pan_in", Error: syntax error    saw 'a constant' near 'proc_level'
spin: line  25 "pan_in", Error: proctype process not found

mtype = {proc_level , msg_level};
/* The first element symbolizes the level */
proctype process(byte proc_level)
{
byte msg_level;
if
    :: com_chan ! proc_level;   /* Send */
    :: com_chan ? msg_level ;   /* Receive */
        if
        :: msg_level > proc_level ->   /* If the level of msg is higher than the level of process */
            assert(false)                    /* Flag an error */
        :: else                               /*Normal operation*/
        fi
    fi
}
prctype proc (byte lvl)
{
:: com_chan ? proc_level(lvl);    /* Send */
:: com_chan ! msg_level(lvl);  /* Receive */
}

init {
chan com_chan = [1] of {byte, mtype }
atomic{
run process();
run proc();
}
}

Offline

#10 2012-09-13 22:55:36

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Verify security properties using model checking technique in Promela

you defined 'proc_level' as a symbolic mtype name
that means that you can then no longer use it as a parameter or variable name
(notice the parameter name for proctype 'process'
same with msg_level -- it is a predefined mtype name (first line)
so you cannot then use it later also as a variable name (byte msg_level)

you also have 'prctype' which is not a keyword (should be proctype)
and you declare a 'proc' with parameter lvl -- but when you instantiate 'proc' you fail to pass the parameter value
(same with the other process instantiation)
quite a few syntax issues to straighten out here -- see http://spinroot.com/spin/Man/

Offline

#11 2012-09-16 06:14:26

Mirza
Member
Registered: 2012-08-30
Posts: 6

Re: Verify security properties using model checking technique in Promela

Fengl_lei_76 thanx mate you gave a good solution to the problem... I have followed it and the mechanism looks fine but a problem is I cannot give different message levels in the same process
I have written the overall mechanism with message level and process level , but in that case msg_level and process_level is same, which doesn't serve the purpose of defining it differently
what my code does is it first sends the message level compares it with process level and if its true then sends, that means message_level and process level is same for a particular process..........if I want different message level for a particular process....how would that be possible......??

Your forum is helping me a lot to experiment thanks to SPIN for the support , Many thanks

===================this is my piece of trial =======================
mtype {prodid, price,creditcard,received,receipt};
chan com_chan_cs = [1] of {byte};
chan com_chan_sp = [1] of {byte};
chan com_chan_spf = [1] of {byte};
chan com_chan_sb = [1] of {byte};
chan com_chan_bc = [1] of {byte};

chan client2store = [1] of {mtype, mtype,byte, byte};
chan store2client = [1] of  {mtype, mtype, byte , byte};
chan store2provider =[1] of {mtype, mtype,byte,byte};
chan provider2store =[1] of {mtype, mtype,byte,byte};

chan store2bank = [1] of  {mtype, mtype, byte , byte};
chan bank2client = [1] of  {mtype, mtype, byte , byte};
chan client2bank = [1] of {mtype, mtype,byte, byte};
chan bank2store = [1] of  {mtype, mtype, byte , byte};

proctype client(byte cproc_level)
{
/* different message level in the same process*/
byte smsg_level;
byte bmsg_level;
byte cmsg_level = cproc_level;/*here we are equating both these */
/* For store */
com_chan_cs ! cmsg_level;
client2store ! prodid,price ;

/* For bank */

com_chan_bc ? bmsg_level;
if
:: bmsg_level < cproc_level ->
         assert(false)                    /* Flag an error */
:: else ->                              /*Normal operation*/

bank2client ? price;

com_chan_bc ! cmsg_level;
client2bank ! creditcard;

    com_chan_cs ? smsg_level;
    if
    :: smsg_level < cproc_level ->
              assert(false)                    /* Flag an error */
    :: else ->                              /*Normal operation*/
    store2client ? prodid,receipt;
    fi
fi

}

proctype store (byte sproc_level)
{
byte cmsg_level;
byte prmsg_level;
byte bmsg_level;

byte smsg_level = sproc_level;
com_chan_cs ? cmsg_level;
/* From client */

if
:: cmsg_level > sproc_level ->
         assert(false)                    /* Flag an error */
:: else ->                              /*Normal operation*/
client2store ? prodid,price;
com_chan_sp ! smsg_level;
store2provider ! prodid,price;

    /* From provider */
    com_chan_spf ? prmsg_level;
    if
    :: prmsg_level < sproc_level ->
              assert(false)                    /* Flag an error */
              :: else   ->                       /*Normal operation*/

        bit flag;
        provider2store ? flag;
        if
        :: flag == 0 ->
                  assert(false)                    /* Flag an error */
                  :: else ->                         /*Normal operation*/
   
        com_chan_sb ! smsg_level;
        store2bank ! prodid,price;

            /* From bank */

            com_chan_sb ? bmsg_level;
            if
            :: bmsg_level < sproc_level ->
                      assert(false)                    /* Flag an error */
            :: else ->                       /*Normal operation*/

            bank2store ? received;
       
            com_chan_cs ! smsg_level;
            store2client ! prodid,receipt;

            fi
        fi

    fi

fi
}
proctype provide (byte prproc_level)
{
bit flag=1;
byte smsg_level;
byte prmsg_level = prproc_level;
com_chan_sp ? smsg_level;

if
:: smsg_level > prproc_level ->
            assert(false)                    /* Flag an error */
          :: else ->                              /*Normal operation*/
store2provider ? prodid,price;

com_chan_spf ! prmsg_level;
provider2store ! flag;
fi

}


proctype bank (byte bproc_level)
{
byte smsg_level;
byte cmsg_level;
byte bmsg_level = bproc_level;

/* For store */
com_chan_sb ? smsg_level;
if
:: smsg_level > bproc_level ->
            assert(false)                    /* Flag an error */
          :: else  ->                             /*Normal operation*/
store2bank ? prodid,price;

/* For client */

com_chan_bc ! bmsg_level;
bank2client ! price;

    com_chan_bc ? cmsg_level;
    if
    :: cmsg_level > bproc_level ->
              assert(false)                    /* Flag an error */
              :: else  ->                             /*Normal operation*/
    client2bank ? creditcard;

    /* For store */
    com_chan_sb ! bmsg_level;
    bank2store ! received;

    fi
fi

}


init {
atomic{
run client(0);
run store(1);
run provide(2);
run bank(3);

}
}

cheers, I'm enjoying it

Offline

#12 2012-09-21 08:52:55

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Verify security properties using model checking technique in Promela

I am glad for you because you have made progress for your problem.  For the remaining problem of flexible msg level, can you simply assign a new value to the variable?  For example, in process client, you can have a line like cmsg_level = cproc_level + 1.  I don't know what is the valid number of cmsg_level.

Offline

Board footer

Powered by FluxBB