A- Consider a program with two inputs and two outputs. (Lo, Ho) = Prog(Li, Hi).

 A- Consider a program with two inputs and two outputs. (Lo, Ho) = Prog(Li, Hi). Input Hi is a high confidentiality input and input Li is a low confidentiality input, and Ho is a private output and Lo is a public output. We say that there is information flow from input Hi to output Lo when which of the following is true?

1.    There exist inputs Li, Hi, Li', Hi' such that running the program on Prog(Li, Hi) produces outputs (Lo, Ho) and running Prog(Li', Hi') produces outputs (Lo', Ho') with Lo' different from Lo

2.    There exist inputs Li, Hi, Hi' such that running the program on Prog(Li, Hi) produces outputs (Lo, Ho) and running Prog(Li, Hi') produces outputs (Lo', Ho') with Lo' different from Lo

3.    There exist inputs Li, Hi, Hi' such that running the program on Prog(Li, Hi) produces outputs (Lo, Ho) and running Prog(Li, Hi') produces outputs (Lo, Ho'), so both have the same public output Lo

4.      For all inputs Li, Hi, Hi' running the program on Prog(Li, Hi) produces outputs (Lo, Ho) and running Prog(Li, Hi') produces outputs (Lo, Ho'), so both have the same public output Lo

B - Imagine that we are looking to verify a function that makes a deep copy of a linked list. That is, the input list is preserved, and a copy is allocated, with the same data elements but appearing in freshly allocated memory cells that don't overlap with the old list. Which of these Hoare triples gives a proper specification?

1.    {list(p)} q = copy(p); {list(p) * list(q)}

2.    {list(q)} q = copy(p); {list(p) * list(q)}

3.    {list(p)} q = copy(p); {list(q)}

4.      {list(q)} q = copy(p); {list(p)}

C - We introduced a general rule for the operation of reading from a pointer: {x => v} y = *x; {x => v && y = v} (We write "&&"

where a di????erent logical "and" operator appears in the slides.) The rule requires some important side conditions.

Assuming that x, y, and v are distinct program variables, which of the following expressions for v would lead to a wrong

conclusion by the rule as given, without side conditions? (Such a case must necessarily be violating the side conditions!)

·       x

·       y

·       x+1

·       y+1