Tarkvara turvalisus 2025/26 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 lecture?

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.
• Try some alternative implementation, like r := -1 * r if r < 0.

During the Labs

We will solve some exercises by Conor Reynolds. The submission site will appear here soon. There will also be a larger tutorial that those really interested in learning Dafny can do as bonus homework.