Security policy for `$Gamma_Global_*` variables?

[aaronbembenek]

I tried running Basil on this C program using the options --simplify --dsa= --dsa-split --dsa-checks --memory-transform:

int x;

int main() {
    return x ? 42 : 0;
}

with this spec:

Globals:
x: bv32

L: x -> true

Here's a fragment of the Boogie code Basil generates:

var {:extern} $Gamma_Global_4325420_4325424: bool;
var {:extern} $Gamma_mem: [bv64]bool;
var {:extern} $Global_4325420_4325424: bv32;
var {:extern} $mem: [bv64]bv8;
const {:extern} $x_addr: bv64;
axiom ($x_addr == 4325420bv64);

...

procedure p$main_4196164(#R0_in: bv64, #Gamma_R0_in: bool, #R1_in: bv64, #Gamma_R1_in: bool, #R30_in: bv64, #Gamma_R30_in: bool, #_PC_in: bv64, #Gamma__PC_in: bool) returns (#R0_out: bv64, #Gamma_R0_out: bool);
  free requires (memory_load64_le($mem, 4325400bv64) == 0bv64);
  free requires (memory_load64_le($mem, 4325408bv64) == 0bv64);
  free requires (memory_load32_le($mem, 4196220bv64) == 131073bv32);
  free ensures (memory_load32_le($mem, 4196220bv64) == 131073bv32);

implementation p$main_4196164(#R0_in: bv64, #Gamma_R0_in: bool, #R1_in: bv64, #Gamma_R1_in: bool, #R30_in: bv64, #Gamma_R30_in: bool, #_PC_in: bv64, #Gamma__PC_in: bool) returns (#R0_out: bv64, #Gamma_R0_out: bool)
{
  var #Exp14__5_22_1: bv32;
  var #Gamma_Exp14__5_22_1: bool;
  var #Gamma_R0_9: bool;
  var #R0_9: bv64;
  b#main_entry:
    assume {:captureState "main_entry (6JJvkaLhTaWXaEL0+yxKxg==)"} true;
    #Exp14__5_22_1, #Gamma_Exp14__5_22_1 := $Global_4325420_4325424, $Gamma_Global_4325420_4325424;
    assert #Gamma_Exp14__5_22_1;
    goto b#phi_1, b#phi_2;
  ...

assert #Gamma_Exp14__5_22_1; fails because $Gamma_Global_4325420_4325424 is unconstrained; however, we know from the spec that x -- aka $Global_4325420_4325424, if I understand things correctly -- should be low security. It seems like the code that Basil generates does not correctly reflect the specified security policy.

Thanks!

global.zip

[l-kent]

This is a bug with the --memory-transform flag - the transform currently doesn't properly take into account the L predicate. I'll look into fixing this.

[ailrst]

Part of the problem is the backend only recognises stores to these variables as side effects

BASIL/src/main/scala/translating/IRToBoogie.scala

Lines 910 to 915 in 44616ee

	case m: MemoryAssign =>
	val lhs = m.lhs.toBoogie
	val rhs = m.rhs.toBoogie
	val lhsGamma = m.lhs.toGamma
	val rhsGamma = exprToGamma(m.rhs)
	List(AssignCmd(List(lhs, lhsGamma), List(rhs, rhsGamma)))

but it will probably also need more information passed from the transform as you suggest, to interpret and use the L predicate correctly for transformed regions.

[l-kent]

I've had a look at that and it's not really related to the issue here at all.