[Dafnyutils] Implement GNU mkfifo

[jkkms]

이름 Your Name

김민성

작업물 Your work

prosyslab/dafnyutils#42

Detailed Description

Korean version

GNU mkfifo 명령어를 Dafny로 구현하고, 동작을 정확히 적은 명세와 구현이 그 명세를 지킨다는 증명을 함께 추가했습니다.

mkfifo는 FIFO(이름 있는 파이프)라는 특수 파일을 만듭니다. FIFO는 내용을 저장하지 않고, 한 프로그램이 쓴 데이터를 다른 프로그램이 읽어 가는 통로 역할만 합니다. mkfifo a b처럼 이름을 여러 개 주면 순서대로 하나씩 만들고, -m 옵션으로 새 FIFO의 권한을 정할 수 있습니다. 권한은 644처럼 숫자(8진수)로 줄 수도 있고, u+x(소유자에게 실행 권한 추가)처럼 기호로 줄 수도 있습니다.

가장 어려웠던 부분은 이 기호 모드였습니다. u+x,g=u, =rw,+x, +644처럼 조합이 다양하고, u+r,(끝 쉼표)처럼 거부해야 하는 문자열도 많습니다. 게다가 대상(u, g, o, a)을 생략하면 umask(새 파일에서 기본으로 빼는 권한)를 반영해야 해서, 같은 +x라도 환경에 따라 결과가 달라집니다.

명세

명세에는 실행 전후 상태를 비교하는 twostate predicate로 어떤 실행이 올바른지 적었습니다. 전체 명세는 MkfifoSpec.Spec입니다.

-m의 값은 이름을 처리하기 전에 한 번만 판단합니다. 값이 문법에 맞지 않으면 mkfifo: invalid mode, setuid 같은 특수 권한이 들어가면 mkfifo: mode must specify only file permission bits를 출력하고, FIFO를 하나도 만들지 않은 채 종료 코드 1을 반환해야 합니다. 종료 코드는 실행이 성공했는지(0) 실패했는지(1)를 알려 주는 값입니다.

이름마다 할 일도 정확히 정했습니다. -m이 없으면 권한 0666으로 FIFO를 만드는 요청 한 번뿐입니다. 이때 운영체제가 umask를 빼므로 보통 0644가 됩니다. -m이 있으면 계산한 권한으로 만든 뒤, 성공했을 때만 권한 변경을 한 번 더 요청합니다. 생성할 때 운영체제가 umask를 빼기 때문에, 사용자가 지정한 권한을 그대로 맞추려면 다시 바꿔야 합니다. 이 권한 변경은 심볼릭 링크를 따라가지 않습니다(GNU의 lchmod).

한 이름이 실패해도 다음 이름은 계속 처리하고, 이미 만든 FIFO는 되돌리지 않습니다. 오류 메시지는 이름 순서대로 표준 오류에 쓰고, 하나라도 실패하면 종료 코드는 1입니다. 변하지 않아야 하는 것도 적었습니다. 모드가 거부되면 파일 시스템이 그대로여야 하고, 표준 출력에는 아무것도 쓰면 안 됩니다.

기호 모드는 문자열을 해석하는 알고리즘을 명세에 넣지 않고 세 부분으로 나눠 적었습니다.

• 문법 트리: 모드를 절의 목록으로 나타냅니다. 절 하나는 대상과, 연산자(+, -, =)와 권한 글자의 묶음으로 이루어집니다.
• Render: 트리를 문자열로 적는 함수입니다.
• Meaning: 트리가 0666에서 시작해 어떤 권한을 만드는지 계산하는 함수입니다.

어떤 문자열이 올바른 모드라는 것은 그 문자열로 적히는 트리가 있다는 뜻이고, 결과 권한은 그 트리의 Meaning입니다. 그런 트리가 하나도 없으면 invalid mode입니다. 문자열을 트리로 바꾸는 일은 구현의 파서가 맡습니다.

구현

파일	역할
MkfifoSchema.dfy	명령줄의 모양(-m 값과 이름 목록)을 정합니다.
MkfifoSpec.dfy	모드의 문법·의미와 전체 명세입니다.
MkfifoModeCore.dfy	모드 문자열을 문법 트리로 바꾸는 파서입니다.
MkfifoModeProof.dfy	파서가 Render를 정확히 거꾸로 계산한다는 증명입니다.
MkfifoCore.dfy	모드를 정하고 이름을 하나씩 처리한 뒤 오류 메시지를 씁니다(RunCore).
MkfifoProof.dfy	반복문의 중간 상태를 명세와 잇는 보조 정리입니다.
Mkfifo.dfy 등	옵션 해석, --help, --version과 실행 진입점입니다.
Tests.py	GNU와 결과를 비교하는 실행 테스트 145건입니다.

RunCore는 먼저 -m 값을 파서에 넣어 모드를 정합니다. 그다음 이름마다 생성을 요청하고, 결과(성공, 생성 실패, 권한 변경 실패)에 맞는 오류 메시지를 모아 둡니다. 모든 이름을 처리하면 모은 메시지를 표준 오류에 한 번에 씁니다.

퍼저(무작위 입력으로 GNU와 결과를 비교하는 도구)에는 mkfifo용 입력 생성기를 추가했습니다. 기존 퍼저는 실행 뒤 파일 시스템을 기록하다가 FIFO를 만나면 오류를 냈습니다. FIFO는 열면 반대쪽이 열릴 때까지 멈출 수도 있어서, 열지 않고 종류·권한 같은 정보만 기록하도록 공용 코드를 조금 고쳤습니다.

예시

umask가 022일 때 다음 명령을 실행합니다. missing 폴더는 없습니다.

mkfifo -m u+x,g=u a missing/b c

먼저 모드를 계산합니다. 권한은 소유자(u), 그룹(g), 나머지(o)마다 읽기(r=4), 쓰기(w=2), 실행(x=1)을 더한 숫자 세 자리로 적습니다.

단계	권한	설명
시작	666	mkfifo의 기본값 a=rw(모두 읽기·쓰기)
u+x	766	소유자에게 실행 권한을 더합니다.
g=u	776	그룹 권한을 지금의 소유자 권한(rwx)과 같게 맞춥니다.

결과 776에는 특수 권한이 없으므로 이름을 처리합니다.

이름	요청	결과	오류 메시지
a	776으로 생성한 뒤 776으로 권한 변경	생성 직후에는 umask가 빠진 754, 변경 뒤 776	없음
missing/b	776으로 생성	실패, 권한 변경은 요청하지 않음	mkfifo: cannot create fifo 'missing/b': No such file or directory
c	a와 같음	776	없음

missing/b가 실패해도 c는 만들어지고, 종료 코드는 1입니다. 표준 출력은 비어 있습니다.

대상을 생략하면 umask가 반영됩니다. umask 022에서 -w는 umask가 막는 그룹·나머지의 쓰기 권한은 그대로 두고 소유자의 쓰기 권한만 빼서 466이 됩니다. +x는 umask에 실행 권한이 없으므로 모두에게 실행 권한을 더해 777이 됩니다. u+s나 4644처럼 특수 권한이 생기는 모드는 아무것도 만들지 않고 오류를 냅니다.

위 결과는 모두 저장소에 고정된 GNU 빌드로 직접 실행해 확인했습니다.

증명

RunCore가 Spec을 만족한다는 것을 증명했습니다. 이름을 처리하는 반복문에서는 다음 조건이 처음에 성립하고, 이름 하나를 처리한 뒤에도 유지된다는 것을 보였습니다.

• 지금까지 처리한 이름마다 명세가 정한 요청만 했습니다.
• 모아 둔 오류 메시지는 처리한 이름들의 메시지를 순서대로 이어 붙인 것입니다.
• 지금까지의 종료 코드는 실패한 이름이 하나라도 있으면 1, 없으면 0입니다.

모드 파서는 Render의 역함수라는 것을 증명했습니다. 올바른 트리를 문자열로 적었다가 다시 파싱하면 원래 트리가 나오고, 파서가 트리를 돌려주면 그 트리를 적은 문자열이 입력과 같습니다. 파서가 실패하면 그 문자열로 적히는 트리가 없다는 것도 보였습니다. 따라서 invalid mode 판단이 정확하고, 올바른 모드의 의미는 하나로 정해집니다.

종료는 파서에서는 남은 문자열의 길이로, 반복문에서는 남은 이름의 수로 증명했습니다.

저장소의 공식 설정(단언마다 따로 검증, 검증 조건당 30초, 선언당 100초)에서 선언 85개, 검증 조건 955개가 모두 통과했습니다. 이 제한 안에 들어오도록 입출력 계약은 불투명한 보조 술어로 감싸고, 반복문의 상태는 술어 하나로 묶었습니다.

명세가 틀린 구현을 거부하는지

명세가 올바른 실행은 받아들이고 틀린 실행은 거부하는지도 확인했습니다. 검증된 구현의 결과가 테스트 145건과 퍼징 3,000건에서 모두 GNU와 일치하므로, 이 입력들에서 GNU의 실제 실행은 명세를 만족합니다.

틀린 실행을 거부하는지는 구현을 한 군데씩 일부러 틀리게 바꾼 16가지 버전으로 확인했습니다. 예를 들어 -m이 없는데도 권한 변경을 요청하거나, 실패한 뒤 남은 이름을 건너뛰거나, 오류 메시지 순서를 뒤집거나, 표준 출력에 한 줄을 쓰는 버전입니다. 16가지 모두 명세 쪽 조건에서 검증에 실패했고, 바꾸지 않은 원래 구현은 통과했습니다.

범위에서 뺀 것

SELinux 보안 문맥을 정하는 -Z와 --context는 뺐습니다. Dafny 쪽 입출력 모델에 보안 문맥을 다루는 기능이 없기 때문이며, 저장소의 mkdir과 같은 결정입니다.

English version

I implemented GNU mkfifo in Dafny, together with a specification that states its behavior precisely and a proof that the implementation meets it.

mkfifo creates special files called FIFOs (named pipes). A FIFO stores no contents; it only passes data written by one program to another program that reads it. Given several names, as in mkfifo a b, it creates them one by one in order, and the -m option sets the permissions of the new FIFOs. A permission can be written as a number (octal), such as 644, or symbolically, such as u+x (add execute permission for the owner).

The hardest part was the symbolic mode. There are many combinations, such as u+x,g=u, =rw,+x and +644, and many strings that must be rejected, such as u+r, with a trailing comma. Moreover, when the target (u, g, o, a) is omitted, the umask (the permissions removed from new files by default) applies, so the same +x can give different results in different environments.

Specification

The specification uses a twostate predicate, which relates the states before and after execution, to state which executions are correct. The overall specification is MkfifoSpec.Spec.

The -m value is judged once, before any name is processed. If it does not follow the syntax, mkfifo must print mkfifo: invalid mode; if it includes special bits such as setuid, it must print mkfifo: mode must specify only file permission bits. In both cases it creates no FIFO and returns exit status 1. The exit status tells whether the run succeeded (0) or failed (1).

The work for each name is also fixed exactly. Without -m, there is a single request to create the FIFO with permissions 0666; the operating system removes the umask, which usually gives 0644. With -m, mkfifo creates the FIFO with the computed permissions and then, only if that succeeded, requests one permission change. Because the operating system removes the umask at creation, the permissions must be set again to match the requested mode exactly. This change does not follow symbolic links (GNU's lchmod).

A failure for one name does not stop the remaining names, and FIFOs already created are kept. Error messages go to standard error in name order, and the exit status is 1 if any name failed. The specification also states what must not change: the filesystem stays the same when the mode is rejected, and nothing is written to standard output.

Instead of putting a string-parsing algorithm into the specification, I described the symbolic mode in three parts.

• Syntax tree: a mode is a list of clauses. Each clause consists of targets and groups of an operator (+, -, =) and permission letters.
• Render: writes a tree as a string.
• Meaning: computes the permissions a tree produces, starting from 0666.

A string is a valid mode when some tree is written as that string, and the resulting permissions are that tree's Meaning. If no tree is written as that string, the mode is invalid. Turning strings into trees is the job of the parser in the implementation.

Implementation

File	Role
MkfifoSchema.dfy	Defines the command-line shape (the -m value and the names).
MkfifoSpec.dfy	Mode syntax and meaning, and the overall specification.
MkfifoModeCore.dfy	Parser that turns a mode string into a syntax tree.
MkfifoModeProof.dfy	Proof that the parser exactly inverts Render.
MkfifoCore.dfy	Decides the mode, processes each name and writes the error messages (RunCore).
MkfifoProof.dfy	Lemmas connecting the loop's intermediate state to the specification.
Mkfifo.dfy and others	Option parsing, --help, --version and the entry point.
Tests.py	145 runtime tests comparing the results with GNU.

RunCore first passes the -m value to the parser to decide the mode. It then requests creation for each name and collects the error message that matches each result (success, creation failure, or permission-change failure). After all names are processed, it writes the collected messages to standard error at once.

I also added a mkfifo input generator to the fuzzer (a tool that compares results with GNU on random inputs). The existing fuzzer raised an error when it met a FIFO while recording the filesystem after a run. Opening a FIFO can block until the other end is opened, so I changed the shared code slightly to record a FIFO's metadata, such as its kind and permissions, without opening it.

Example

Run the following command with umask 022. The missing directory does not exist.

mkfifo -m u+x,g=u a missing/b c

The mode is computed first. Permissions are written as three digits, one each for the owner (u), group (g) and others (o), each the sum of read (r=4), write (w=2) and execute (x=1).

Step	Mode	Explanation
Start	666	mkfifo's default a=rw (read and write for everyone)
u+x	766	Adds execute permission for the owner.
g=u	776	Sets the group permissions to the owner's current permissions (rwx).

The result 776 has no special bits, so the names are processed.

Name	Requests	Result	Error message
a	Create with 776, then change the mode to 776	754 right after creation (umask removed), 776 after the change	None
missing/b	Create with 776	Fails; no permission change is requested	mkfifo: cannot create fifo 'missing/b': No such file or directory
c	Same as a	776	None

c is still created after missing/b fails, and the exit status is 1. Standard output stays empty.

When the target is omitted, the umask applies. With umask 022, -w leaves the group and others' write permissions, which the umask protects, unchanged and removes only the owner's, giving 466. +x adds execute permission for everyone, giving 777, because the umask contains no execute bits. A mode that produces special bits, such as u+s or 4644, creates nothing and reports an error.

I checked all of these results by running the GNU build pinned in the repository.

Proof

I proved that RunCore satisfies Spec. For the loop over names, I showed that the following conditions hold initially and still hold after each name is processed:

• For every name processed so far, only the requests fixed by the specification were made.
• The collected error messages are the messages of the processed names, concatenated in order.
• The exit status so far is 1 if any processed name failed and 0 otherwise.

I proved that the mode parser is the inverse of Render. Writing a valid tree as a string and parsing it again gives back the original tree, and when the parser returns a tree, writing that tree gives the input string. When the parser fails, no tree is written as that string. Therefore the invalid mode decision is exact, and a valid mode has exactly one meaning.

Termination follows from the length of the remaining string in the parser and from the number of remaining names in the loop.

Under the repository's official settings (each assertion verified separately, 30 seconds per verification condition, 100 seconds per declaration), all 85 declarations and 955 verification conditions pass. To fit within these limits, I wrapped the IO contracts in opaque helper predicates and grouped the loop state into a single predicate.

Does the specification reject incorrect implementations?

I also checked that the specification accepts correct executions and rejects incorrect ones. The verified implementation matches GNU on all 145 tests and 3,000 fuzzing cases, so GNU's actual executions on these inputs satisfy the specification.

To check rejection, I made 16 versions of the implementation, each deliberately wrong in one place. For example, one requests a permission change even without -m, one skips the remaining names after a failure, one reverses the order of error messages, and one writes a line to standard output. All 16 fail verification at a condition of the specification, while the unchanged implementation passes.

Left out

-Z and --context, which set the SELinux security context, are left out. The Dafny IO model has no operation for security contexts; the repository's mkdir makes the same decision.