New Posts

This commit is contained in:
Brandon Rozek 2022-02-05 00:50:07 -05:00
parent 60dba11acc
commit 55f752a173
4 changed files with 266 additions and 0 deletions

111
content/blog/dafny-loops.md Normal file
View file

@ -0,0 +1,111 @@
---
title: "Reasoning through Loops in Dafny"
date: 2022-02-05T00:22:58-05:00
draft: false
tags: []
math: true
---
Dafny treats loops like a black box. It could be annoying the first time you experience this and have no clue why the code is not verifying properly. There are two properties that Dafny needs you to prove: partial correctness and termination. Together these form *total correctness*.
## Partial Correctness
Partial correctness is concerned with whether the system is sound and complete. In other words, if the loop terminates that the postcondition holds for all possible inputs constrained by the precondition.
```csharp
method arrayUpToN(n: int) returns (a: array<int>)
requires n >= 0
ensures a.Length == n
ensures forall j :: 0 < j < n ==> a[j] >= 0
ensures forall j, k : int :: 0 <= j <= k < n ==> a[j] <= a[k]
{
var i := 0;
a := new int[n];
while i < n
{
a[i] := i;
i := i + 1;
}
}
```
In order to solve this, we need to concept of a loop invariant. A loop invariant is a formula that is true before, during, and after the loop. In order to prove the postcondition, we need to choose the relevant loop invariants such that:
$$
\neg Loop\_Condition \wedge Loop\_Invariants \implies Post\_Condition
$$
If this is not the case, then Dafny will likely complain to you as it has no clue what's going on. Here are the invariants you need to add in order for it to verify:
```csharp
invariant 0 <= i <= n
invariant forall k :: 0 <= k < i ==> a[k] >= 0
invariant forall k :: 0 <= k < i ==> a[k] == k
invariant forall j, k :: 0 <= j <= k < i ==> a[j] <= a[k]
```
Together this forms:
```csharp
method arrayUpToN(n: int) returns (a: array<int>)
requires n >= 0
ensures a.Length == n
ensures forall j :: 0 < j < n ==> a[j] >= 0
ensures forall j, k : int :: 0 <= j <= k < n ==> a[j] <= a[k]
{
var i := 0;
a := new int[n];
while i < n
invariant 0 <= i <= n
invariant forall k :: 0 <= k < i ==> a[k] >= 0
invariant forall k :: 0 <= k < i ==> a[k] == k
invariant forall j, k :: 0 <= j <= k < i ==> a[j] <= a[k]
{
a[i] := i;
i := i + 1;
}
}
```
## Termination
Termination is concerned with whether your loop will finish in finite time. The way that Dafny does this is by guessing what is called the Decrementing function. In Dafny, the decrementing function is required to:
- Decrease with each iteration of the loop
- Be bounded below by zero
In the last example, Dafny was able to correctly guess that decrementing function was $n - i$. What about the following example:
```csharp
method fact(x: int) returns (y: int)
requires x >= 0
{
var z := 0;
y := 1;
while z != x
invariant 0 <= z <= x
{
z := z + 1;
y := y * z;
}
}
```
Turns out in this scenario, Dafny was not able to successfully guess. To supply it with the decrementing function use the keyword `decreases`.
```csharp
method fact(x: int) returns (y: int)
requires x >= 0
{
var z := 0;
y := 1;
while z != x
decreases x - z
invariant 0 <= z <= x
{
z := z + 1;
y := y * z;
}
}
```

View file

@ -0,0 +1,29 @@
---
title: "Docker Secrets"
date: 2022-02-04T23:59:13-05:00
draft: false
tags: []
math: false
---
I try to keep secrets such as passwords and keys out in their own separate files so that I can `.gitignore` them and commit the rest of my configuration. With `docker-compose` we can do that with the `env_file` field. Here is an example with a postgres configuration:
```yaml
database:
image: postgres:13.4
container_name: database
hostname: database
env_file:
- Volumes/database/docker.env
volumes:
- Volumes/database/var/lib/postgresql/data:/var/lib/postgresql/data
```
Then in `Volumes/database/docker.env` I can have a file with the secrets as key-value pairs:
```yaml
POSTGRES_USER=user
POSTGRES_PASSWORD=389ed93045c84cc0828c4310e6ef76ce
POSTGRES_DB=database
```

View file

@ -0,0 +1,62 @@
---
title: "Program Verification with Hoare Logic and Dafny"
date: 2022-02-05T00:06:42-05:00
draft: false
tags: []
math: false
---
In the recitations that I'm giving for [Principles of Software](https://brandonrozek.com/ta/spring2022/csci2600/), we are going over reasoning through code using Hoare Logic and the program verifier Dafny. Microsoft Research designed Dafny to be similar to writing imperative code. The main difference is that you need to supply (pre/post)-conditions and the code to verify. Here's an example of how to reason about a simple statement by hand:
```csharp
// Precondition: x > 0
x := x + 1;
// Postcondition: x > 1
```
Given the fact that x is greater than zero before the code begins, we can deduce that if we increment it by one then it must be greater than one! Though to showcase Dafny, we'll look at a slightly more interesting (albeit famous beginner example) which is the absolute value:
```csharp
method abs(x: int) returns (y: int)
requires true
ensures y >= 0
ensures x >= 0 ==> x == y
{
if (x < 0) {
y := -x;
} else {
y := x;
}
}
```
The `requires` clause is otherwise known as the precondition or what is known to be true before the method executes. For the case of absolute value, we do not need to constrain any of the integer inputs, so we can put `requires true` or not even include that line.
The `ensures` clause is otherwise known as the postcondition or what you want verified to be true after the method executes. In there we have two conditions: the output must be positive, and if the input was positive then the output equals the input.
Then finally the code goes in the method body.
Now you can actually verify it line by line through the use of `assert` statements. Here's the same method again but with assertions:
```csharp
method abs(x: int) returns (y: int)
requires true
ensures y >= 0;
ensures x >= 0 ==> x == y
{
if (x < 0) {
assert x < 0;
y := -x;
assert y > x;
} else {
assert x >= 0;
y := x;
assert y == x;
}
}
```

64
content/blog/s3-fuse.md Normal file
View file

@ -0,0 +1,64 @@
---
title: "Mount Object Storage Locally using S3 Fuse"
date: 2022-02-04T23:39:25-05:00
draft: false
tags: []
math: false
---
On most cloud providers, object storage is cheaper than paying for the equivalent size in block storage. Using FUSE, we can mount S3 compatible object storage with the command `s3fs`. Do note, that there are a few downsides with mounting object storage as documented on their [README](https://github.com/s3fs-fuse/s3fs-fuse/blob/master/README.md):
- random writes or appends to files require rewriting the entire object, optimized with multi-part upload copy
- metadata operations such as listing directories have poor performance due to network latency
- non-AWS providers may have eventual consistency so reads can temporarily yield stale data (AWS offers read-after-write consistency since Dec 2020)
- no atomic renames of files or directories
- no coordination between multiple clients mounting the same bucket
- no hard links
- inotify detects only local modifications, not external ones by other clients or tools
Lets get started by installing `s3fs`:
```bash
# For Fedora
sudo dnf install s3fs-fuse
# For Ubuntu/Debian
sudo apt install s3fs
```
We'll then need to edit `/etc/passwd-s3fs` with our object storage access and secret keys:
```yaml
AccessKeyHere:SecretKeyHere
```
Then we need to set it so that only root can read `/etc/passwd-s3fs`
```bash
sudo chmod 600 /etc/passwd-s3fs
```
Now we can test to see if we can access our bucket:
```bash
sudo s3fs bucketname \
/mnt/mountpoint \
-o url=https://us-east-1.linodeobjects.com \
-o allow_other
```
If we're successful we should be able to access `/mnt/mountpoint`.
To unmount:
```bash
sudo umount /mnt/mountpoint
```
To mount automatically during reboot, add the following to `/etc/fstab`:
```
bucketname /mnt/mountpoint fuse.s3fs _netdev,allow_other,url=https://us-east-1.linodeobjects.com 0 0
```
After editing `/etc/fstab` you can run `sudo mount -a` in order for it to load and mount any new entries.