ALLOY - How to set value for a signature

Vote count: 0

I want to formalize an access from an application to the data section of other application. Firstly, I create signatures for Request (e.g APP1 wants to READ the DATASECTION of APP2) and Permission (the request A is MAY_PREVENT)

sig request{
 from: OS_App,
 to: Memory,
 act: action
}

sig permission{
    req: request,
    per: status
}

I wrote two functions for my idea, but it does not work. Someone can help me, please?

//Assign a request 
pred P_026 [asc: request, app1: NonTrusted, app2: OS_App, ds: app2.ownDS]{
    asc.from = app1
    asc.to = ds
    asc.act = read
}

//If the Request is A then status is may_prevent
fun F_026[s: status, requ: request, app1: NonTrusted, app2: OS_App, ds: app2.ownDS]: set may_prevent{
    {s : requ.per | requ in P_026[requ,app1,app2,ds]} 
}

asked 36 secs ago

Trình Lê Khánh

Let's block ads! (Why?)

ALLOY - How to set value for a signature