Tarkvara turvalisus 2024/25 kevad

Introduction & Dafny

By the end of this introductory week (which hopefully will last no longer than two weeks), you should be able to

• situate software security in the broader knowledge areas of cyber security,
• advocate passionately for the software security approach, and
• decide if exposure to the underlying theory of verification tools is not your cup of tea!

Background

Ensuring the security of a software-reliant organization involves a range of approaches; the field of cyber security is vast.

• The Introduction to the CyBOK gives a good overview of the knowledge areas of cyber security. Figure 2 summarizes what each area is concerned with.
• What is software security? The CyBOK chapter is useful (webinar), and you may listen to the first two videos from the Hicks's course.

Hands-On Demo

The goal is to get a little bit of hands-on experience with Dafny. First you need to install dafny. It is reasonably easy:

• Install vscode.
• Install the dafny plugin from the marketplace.
• Try to open a file with .dfy extension, it should try to install dotnet.

1. Hello World!

Try create and a new file and name it abs.dfy:

method Abs(i: int) returns (r: int)
ensures 0 <= r
{   
    if 0 <= i {
        r := i;
    } else {
        r := -i;
    }
}

Change the condition to -1 <= i to make sure Dafny complains.

2. Play around with assertions.

Now, you can try to use assertions to narrow down where the post-condition fails. The full tableaux proof for the program would look like this:

method Abs(i: int) returns (r: int)
ensures 0 <= r
{   
    if 0 <= i {
        assert 0 <= i;
        r := i;
        assert 0 <= r;
    } else {
        assert i < 0;
        assert 0 <= -i;
        r := -i;
        assert 0 <= r;
    }
    assert 0 <= r;
}

Can you see how this relates to the theory slides?

3. Adapt to machine integers

Now, add the following to the top of the program to define 32 bit integers:

newtype {:nativeType "int"} int32 = x | -0x8000_0000 <= x < 0x8000_0000

Try to prove the program with this int32 data type. You can add a precondition with the keyword requires. In Java, Math.abs(int) does violate the post-condition in this way, while Math.absExact(int) will thrown and exception.

4. Partial Specifications

This the above is not a proper specification of the absolute value function.

• Change the method to satisfy the current specification in a more stupid way...
• Update the specification to fully say that it should be related to the input in some way.

To Be Continued ...

We will return to Dafny after having understood what it was used to implement.