Some applications depend on file system support for accurate (or at least monotonic) modification times in stat.

Hi, very nice project!

Next week I will be at the 11th MirageOS retreat; my project for the week would be to try to look at FSCQ and see how hard it would be to extract it to OCaml and package it as a MirageOS-compatible library.
I've only quickly looked at the makefile/build instructions currently; it looked to me that there there is some existing setup for OCaml extraction but that ExtractOcaml.v might be outdated?

More generally speaking, I wondered if you'd have any relevant advice that could be helpful for the task :-).
I'm also interested on any information on the structure of the development / what are the entrypoints of the Coq library / the API that should be exposed or not, if you have :-).

Does fscq support sync() system call?
If so, there seems to be a bug which makes sync fail to persist new directory entries. This correspondingly causes an inconsistent file system state after a crash.

Below describes the test case that triggers the bug.

1. After mounting an empty fscq image:

$ mkdir /tmp/fscqmnt
$ ./fscq/src/fscq empty.img -f -o big_writes,atomic_o_trunc,use_ino /tmp/fscqmnt

2. Run the PoC which creates a directory, calls sync, then crashes fscq daemon.
   PoC:

#include <sys/types.h>
#include <sys/stat.h>
#include <sys/syscall.h>
#include <stdlib.h>
#include <unistd.h>

int main(int argc, char *argv[])
{
    chdir("/tmp/fscqmnt");
    system("ls");
    system("ls");
    system("ls");
    system("ls");
    system("ls");
    system("tree");

    syscall(SYS_mkdir, "foo", 0777);
    syscall(SYS_sync);
    system("killall -9 fscq"); // crash fscq

    return 0;
}

3. Re-mount the image on another directory

$ mkdir /tmp/fscqmnt2
$ ./fscq/src/fscq empty.img -f -o big_writes,atomic_o_trunc,use_ino /tmp/fscqmnt2

4. Check inconsistency (foo is not persisted)

$ ls /tmp/fscqmnt2
$ ls /tmp/fscqmnt2
$ ls /tmp/fscqmnt2
$ tree /tmp/fscqmnt2
/tmp/fscqmnt2

0 directories, 0 files

Hi, our team at SSLab, Georgia Tech is fuzz testing various file systems for crash consistency bugs. While testing FSCQ, we found a potential crash consistency bug. Could you take a look at the test case we have?

1. Mount an empty image:

$ mkdir /tmp/fscqmnt
$ ./fscq/src/fscq empty.img -f -o big_writes,atomic_o_trunc,use_ino /tmp/fscqmnt

2. Compile and run the test case:

#include <sys/types.h>
#include <sys/stat.h>
#include <sys/syscall.h>
#include <stdlib.h>
#include <unistd.h>
#include <fcntl.h>

int main(int argc, char *argv[])
{
        chdir("/tmp/fscqmnt");
        system("ls");
        system("ls");
        system("ls");
        system("ls");
        system("ls");
        system("tree");

        unsigned char buf[8192] = { 0, };
        int fd_root = syscall(SYS_open, ".", O_DIRECTORY, 0);
        int fd_foo = syscall(SYS_open, "./foo", O_CREAT | O_RDWR, 0777);
        syscall(SYS_fsync, fd_foo);
        syscall(SYS_mkdir, "./A", 0777);
        syscall(SYS_ftruncate, fd_foo, 5595);
        syscall(SYS_pwrite64, fd_foo, buf, 4000, 1303);
        syscall(SYS_fsync, fd_root);

        system("killall -9 fscq"); // crash fscq
        return 0;
}

3. Re-mount the image on another directory

$ mkdir /tmp/fscqmnt2
$ ./fscq/src/fscq empty.img -f -o big_writes,atomic_o_trunc,use_ino /tmp/fscqmnt2

4. Check inconsistency (directory A is missing)

$ tree /tmp/fscqmnt2
fscqmnt2
└── foo

0 directories, 1 file

[Description]
If we make a directory "./A" and fsync the root directory ".", the directory entry A is persisted on disk, and is shown after a crash.
However, as in the test case above, if we mkdir A, then perform ftruncate and pwrite on the file descriptor of another file "./foo", fsync'ing the root directory fails to persist directory A.

Any opinion on this?

Thank you,
-Seulbae

Hi, our team at SSLab, Georgia Tech is testing the crash safety property of fscq and we found that fdatasync is not working as expected maybe? Following is the test case:

1. Mount an empty image

mkdir -p mptr1
<path-to-fscq-src>/fscq empty.img -f -o big_writes,atomic_o_trunc,use_ino mptr1

2. Compile and run the test case

#include <stdio.h>
#include <string.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <sys/syscall.h>
#include <stdlib.h>
#include <unistd.h>
#include <fcntl.h>

int main(int argc, char *argv[])
{
        chdir("mptr1");
        system("ls");
        system("ls");
        system("ls");
        system("ls");
        system("ls");
        system("tree");
 
        int rv;
 
        unsigned char buf[8192] = { 0 };
        memset(buf, 'a', 8192);
 
        int fd_foo = syscall(SYS_open, "foo", O_CREAT | O_RDWR, 0777);
        printf("fd: %d\n",  fd_foo);
 
        int fd_mntpnt = syscall(SYS_open, ".", O_DIRECTORY, 0);
        printf("root fd: %d\n", fd_mntpnt);
 
        rv = syscall(SYS_fsync, fd_mntpnt);
        printf("fsync mntpnt: %d\n", rv);
 
        rv = syscall(SYS_write, fd_foo, buf, 4000);
        printf("write: %d\n", rv);
 
        rv = syscall(SYS_fdatasync, fd_foo);
        printf("fdatasync: %d\n", rv);
 
        system("killall -9 fscq"); // crash fscq
        return 0;
}

Output of the test case should be:

.

0 directories, 0 files
fd: 3
root fd: 4
fsync mntpnt: 0
write: 4000
fdatasync: 0

Based on the return code of fsync, write, and fdatasync, file foo should be there with 4000 a in its content.

3. Re-mount the image on another directory

<path-to-fscq-src>/src/fscq empty.img -f -o big_writes,atomic_o_trunc,use_ino mptr2

4. Check inconsistency: file foo is empty

tree mptr2
mptr2
└── foo

0 directories, 1 file

cat mptr2/foo
<nothing returns back>

wc -c mptr2/foo
0 mptr2/foo

[System Setup]
I am seeing this issue on the master branch of the repo although I see this issue in the sosp17 branch as well. I am using Ubuntu 16.04 with 4.4.0 kernel and compiled fscq with coqc 8.8.1 and ghc 8.0.1.

Let me know if you need further information. Thank you!

Some applications depend on file system support for hard links.

On 27c4078, running

#include <stdio.h>
#include <sys/stat.h>
#include <string.h>
#include <errno.h>

int main() {
  int err;

  mkdir("a", 0700);
  mkdir("b", 0700);
  mkdir("b/0",0);
  errno = 0;
  err = rename("a","b");
  if (err < 0) {
    printf("rename error: %s\n",strerror(errno));
    return 1;
  }

  return 0;
}

prints rename error: Input/output error when the rename call should set errno to ENOTEMPTY or EEXIST. This issue is probably related to #3 and approximately as unlikely cause significant issues for applications.

On an empty file system built from 27c4078, running

#include <unistd.h>
#include <fcntl.h>

int main() {
  close(creat("spaaaaaace"));
  truncate("spaaaaaace",10);

  return 0;
}

results in a file, spaaaaaace, which contains the text spaaaaaace instead of 10 null bytes. For applications which expect POSIX, OS X, Linux, or BSD behavior when using truncate to extend files, this unexpected data can result in incorrectly formatted files.

Some security properties of some systems are, at least partially, reliant on file system support for rwx permissions for users, groups, and 'other'. These features are often used in conjunction with multiuser access to a single mounted file system and FS enforcement of user permission policy.

The implementation of ftruncate calls the wrong function in AsyncFS.v, setting the inode size blindly without allocating new blocks if the size grows. Here's a bug that results from implicitly using block 0 for the new blocks:

test-case.c:

#include <fcntl.h>
#include <unistd.h>
#include <stdio.h>

int main() {
  chdir("/tmp/fscqmnt");

  unsigned char buf[2] = { 1, 2 };
  int fd_foo = open("foo", O_CREAT | O_RDWR, 0777);
  ftruncate(fd_foo, 5);
  pwrite(fd_foo, buf, 2, 0);

  int fd_bar = open("bar", O_CREAT | O_RDWR, 0777);
  ftruncate(fd_bar, 5);

  unsigned char rbuf[2];
  pread(fd_bar, &rbuf, 2, 0);
  // BUG: this outputs "bar: 01 02" instead of the expected "bar: 00 00"
  printf("bar: %02d %02d\n", (int) rbuf[0], (int) rbuf[1]);
  close(fd_bar);

  // just to demonstrate what gets written
  sync();

  return 0;
}

bug.sh:

#!/bin/bash

set -e

DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
FSCQ=$HOME/fscq

start_fscq() {
  "$FSCQ"/src/fscq "$FSCQ"/src/disk.img -f -o big_writes,atomic_o_trunc,use_ino "$1" &
  sleep 0.5
}

unmount_fscq() {
  fusermount -u "$1"
}

mkdir -p /tmp/fscqmnt
gcc "$DIR"/test-case.c -o "$DIR"/test-case
if [ ! -f /tmp/empty.img ]; then
  "$FSCQ"/src/mkfs /tmp/empty.img
fi
cp /tmp/empty.img "$FSCQ"/src/disk.img

start_fscq /tmp/fscqmnt
"$DIR"/test-case
tree -s /tmp/fscqmnt
unmount_fscq /tmp/fscqmnt

Running bug.sh (or compiling and running test-case.c after mounting FSCQ to /tmp/fscqmnt) produces bar: 01 02, since foo and bar point to the same disk blocks.

Hi.
While testing FSCQ, I came across this potential logic bug:
Directory A is considered "not empty" after an inode A/foo is created then unlinked, thus prohibiting any other directory from being renamed to A.

To test, first create an empty disk image, and mount it at /tmp/mnt.
Then, compile and run the following PoC:

#include <sys/types.h>
#include <sys/stat.h>
#include <sys/syscall.h>
#include <stdlib.h>
#include <unistd.h>
#include <fcntl.h>
#include <string.h>
#include <stdio.h>
#include <errno.h>

int main(int argc, char *argv[])
{
    chdir("/tmp/mnt");

    syscall(SYS_mkdir, "A");
    int fd_A = syscall(SYS_open, "A", O_DIRECTORY, 0);
    int fd_foo = syscall(SYS_open, "A/foo", O_CREAT | O_RDWR, 0777);
    syscall(SYS_unlink, "A/foo");

    syscall(SYS_fsync, fd_foo);
    syscall(SYS_fsync, fd_A);

    syscall(SYS_mkdir, "B");
    int ret = syscall(SYS_rename, "B", "A");
    if (ret < 0)
        printf("rename B A failed: %d (%s)\n", errno, strerror(errno));
    return 0;
}

The output is rename B A failed: 39 (Directory not empty), even though the directory A is emptied and explicitly fsynced.

$ tree mnt
mnt
├── A
└── B

2 directories, 0 files

On 27c4078, when running:

# touch foo
# ls -l foo
-rwxrwxrwx 1 root root 0 Jan  1  1970 foo
# chmod 700 foo
# ls -l foo
-rwxrwxrwx 1 root root 0 Jan  1  1970 foo

an error such as ENOSYS is expected if chmod is not implemented.

Many applications depend on file system support for symlinks.

On 27c4078, running

$ mkdir foo
$ touch foo/bar
$ rmdir foo

results in rmdir: failed to remove ‘foo’: Input/output error when either EEXIST or ENOTEMPTY is expected in this case. See http://pubs.opengroup.org/onlinepubs/9699919799/functions/rmdir.html for details.

When a subdirectory is created, the parent directory's link count increases by 1 (for ..) on typical POSIX-like file systems. Using 27c4078, a directory's link count remains 2 when subdirectories are created:

# mkdir foo
# stat foo
  File: ‘foo’
  Size: 4096        Blocks: 1          IO Block: 4096   directory
Device: 29h/41d Inode: 8           Links: 2
Access: (0755/drwxr-xr-x)  Uid: (    0/    root)   Gid: (    0/    root)
Access: 1970-01-01 01:00:00.000000000 +0100
Modify: 1970-01-01 01:00:00.000000000 +0100
Change: 1970-01-01 01:00:00.000000000 +0100
 Birth: -
# mkdir foo/bar
# stat foo
  File: ‘foo’
  Size: 4096        Blocks: 1          IO Block: 4096   directory
Device: 29h/41d Inode: 8           Links: 2
Access: (0755/drwxr-xr-x)  Uid: (    0/    root)   Gid: (    0/    root)
Access: 1970-01-01 01:00:00.000000000 +0100
Modify: 1970-01-01 01:00:00.000000000 +0100
Change: 1970-01-01 01:00:00.000000000 +0100
 Birth: -

While many POSIX foreign file systems do not obey directory link count invariants, it can be useful for programs (e.g. find) which perform many directory traversals.