From: Thomas Walker Lynch Date: Fri, 6 Nov 2026 15:04:06 +0000 (+0000) Subject: reorganized manual X-Git-Url: https://git.reasoningtechnology.com/%27%20%20%20window.RT.dirpr_library%20%20%20%27/%27%20%20%20key%20%20%20%27?a=commitdiff_plain;h=6193c41db45352d2acc32b4fab7144468a5ce6c6;p=Man_In_Grey reorganized manual --- diff --git a/document/Man_In_Grey.html b/document/Man_In_Grey.html index 46fd28f..ebd9b86 100644 --- a/document/Man_In_Grey.html +++ b/document/Man_In_Grey.html @@ -95,300 +95,298 @@ The interpreter is invoked by the gate after, and only if, the guard has approved the journal. The interperter walks the journal while executing the instructions in order. - The two user ids a process carries. The effective uid determines what the process is permitted to do, and the real uid identifies the ultimate invoking process's real uid. See . + The two user ids a process carries. The effective uid determines what the process is permitted to do, and the real uid identifies the ultimate invoking process's real uid. See . - - Out-of-band signaling -

- Man_In_Grey provides an alternative to templates. In template systems an output file, such as a configuration file, is generated by a blank filling program. With Man_In_Grey the output file is written by interpreting a journal, and the journal is written by a composer. -

-

- There are problems with the method of filling in templates, for one it mixes data and control together: the content to be written, and the marks that say where to substitute. Thus templating is a form of in-band signaling. With in-band signaling, a content string can be identical to a control string, so data and control can alias, and there is no tight way to design the aliasing out. The typical workaround is to disallow control strings in the data, and to write each disallowed character as an escape sequence, where the escape is then itself control. Each level of nesting multiplies the escapes: an f-string that explains how to write f-strings escapes its braces has twice the number of escapes as the base f-string, and a document about this f-string escapes them again, to have 4 times the number, etc. -

-

- Man_In_Grey signals out of band. A composer is a program, so the logic that forms the output is code, with loops, conditions and lookups, rather than marks embedded in the output. An instruction in the journal is a structure, and file content is carried in it as a byte string with its length. The journal interpreter never scans content for meaning, so content can hold anything, including text that looks like a journal, with no escaping. (A developer is free to create a composer that fills in templates if that is what he really wants; but there is no inherent need to use this approach.) -

-

- The journal is encoded in CBOR, whose strings are length-prefixed. Decoding CBOR makes maps, lists, strings and bytes, and cannot run code, so a journal reaches account B as data and nothing else. -

-

- Man_In_Grey replaces the template, not the syntax of the file being written. Content is still to be well formed for the program that reads the file, so a composer writing HTML escapes a < in its text as HTML requires. An instruction language can take that work over too, as the example in does. -

- + + Concept - - Symbol -

- A composer writes instructions, but it does not run them. When an instruction would produce a result when run, as for example an instruction that makes an account and returns its uid, the result does not exist yet at the time the composer runs. Hence, when an instruction is entered into the journal via the journal interface, the interface returns a symbol placeholder. The symbol is then used as an argument by the composer when it enters instructions that are given said result as an argument. In the current implementation a symbol is simply the index into the journal that locates an instruction. Thus, with the current implementation each instruction can have at most one result. -

- - account = journal_iface.make_account("Thomas·www") - journal_iface.add_to_group(account ,"http") - -

- In this example account is a result symbol. The value of account will be 0, i.e. the index into the journal of the make_account instruction. The two instructions are of a language an application that manages accounts would define; the example language in has no instruction that produces a result. -

- - - - uid -

- Each account has a number called its user id, or uid. Each file has an owner, noted with a uid. Each process is associated with two uids, its real uid and its effective uid. When a person logs in, the login program starts his shell with both uids set to that of his account, and every process started from the shell inherits them. In colloquial speech such processes are said to be owned by the person, or to run under his account. However, the two uids associated with a process can differ, so these colloquialisms are imprecise. -

-

- The effective uid determines a process's permissions. So for example when opening a file, the kernel compares the process's effective uid with a file's owner and permission bits to determine if the process is allowed to open the file. Among its other uses, the kernel lets a process send a signal to another process whose real uid equals its own real or effective uid. -

-

- A process inherits both uids from the process that invoked it, unless the program file it runs has its setuid permission bit set. In which case, the kernel then takes the effective uid from the file's owner instead, while the real uid remains inherited as before. A process therefore gets its effective uid in one of two ways: from the process that invoked it, or from the owner of a setuid program file. (Groups work the same way, with a real gid, an effective gid and a setgid bit, beside the supplementary groups, which are inherited unchanged.) -

-

- By convention, the gate is the only program of Man_In_Grey that can optionally be given the setuid bit. When the gate is not setuid, it inherits its effective and real uids from the program that invoked it. When it is setuid, it inherits its real uid from the program that invoked it, and it inherits its effective uid from its file owner. Thus, the gate process has reliable information directly from the kernel on who invoked it, as that is its real uid. It also has reliable information directly from the kernel on who owned its executable file, as that becomes its effective uid. -

- -

- Due to this mechanism the effective uid for a setuid gate program can be different than the effective uid of the program that invoked it. In the chain of events of program A running and then invoking the gate, the effective uid in that thread of execution will start as the effective uid for program A, and then the effective uid will change to match the uid of the gate executable file owner. We can say that the effective uid change from A to B, where A is the invoking programs effective uid, an B is the owner of the gate executable file. -

- - - - Orchestrator -

- The orchestrator is a utility program provided with Man_In_Grey. The orchestrator calls one or more composer programs, then sends the resulting journal to a gate program. Like all processes, when the orchestrator program runs, it has a real and effective uid. When the orchestrator is run from a shell, these are both inherited from the shell, and are typically pointing to the login user. In any case, the composers that it invokes will then run with the same effective and real uids as the orchestrator. When the gate executable file has its setuid bit set, when the gate is invoke by the orchestrator, the gate will inherit its real uid from the orchestrator, and will take its effective uid from the gate's executable file owner. -

+ + Out-of-band signaling +

+ Man_In_Grey provides an alternative to templates. In template systems an output file, such as a configuration file, is generated by a blank filling program. With Man_In_Grey the output file is written by interpreting a journal, and the journal is written by a composer. +

+

+ There are problems with the method of filling in templates, for one it mixes data and control together: the content to be written, and the marks that say where to substitute. Thus templating is a form of in-band signaling. With in-band signaling, a content string can be identical to a control string, so data and control can alias, and there is no tight way to design the aliasing out. The typical workaround is to disallow control strings in the data, and to write each disallowed character as an escape sequence, where the escape is then itself control. Each level of nesting multiplies the escapes: an f-string that explains how to write f-strings escapes its braces has twice the number of escapes as the base f-string, and a document about this f-string escapes them again, to have 4 times the number, etc. +

+

+ Man_In_Grey signals out of band. A composer is a program, so the logic that forms the output is code, with loops, conditions and lookups, rather than marks embedded in the output. An instruction in the journal is a structure, and file content is carried in it as a byte string with its length. The journal interpreter never scans content for meaning, so content can hold anything, including text that looks like a journal, with no escaping. (A developer is free to create a composer that fills in templates if that is what he really wants; but there is no inherent need to use this approach.) +

+

+ The journal is encoded in CBOR, whose strings are length-prefixed. Decoding CBOR makes maps, lists, strings and bytes, and cannot run code, so a journal reaches account B as data and nothing else. +

+

+ Man_In_Grey replaces the template, not the syntax of the file being written. Content is still to be well formed for the program that reads the file, so a composer writing HTML escapes a < in its text as HTML requires. An instruction language can take that work over too, as the example in does. +

+ -

- The orchestrator finds the composers by file. Given a composer file, or a composer directory, it runs each file, and in each it calls one function, compose(prov ,journal_iface). To the orchestrator a composer is therefore a file: each composer is to be given a file of its own, and the file is to define exactly one function of that form. The file can define other functions as helpers of it, but the orchestrator calls none of them, and a second function meant as a composer is never run. Several composers are several files, and the order of the files in the composer directory, as describes, is the order they run in. -

+ + Real and effective uid +

+ Each account has a number called its user id, or uid. Each file has an owner, noted with a uid. Each process is associated with two uids, its real uid and its effective uid. When a person logs in, the login program starts his shell with both uids set to that of his account, and every process started from the shell inherits them. In colloquial speech such processes are said to be owned by the person, or to run under his account. However, the two uids associated with a process can differ, so these colloquialisms are imprecise. +

+

+ The effective uid determines a process's permissions. So for example when opening a file, the kernel compares the process's effective uid with a file's owner and permission bits to determine if the process is allowed to open the file. Among its other uses, the kernel lets a process send a signal to another process whose real uid equals its own real or effective uid. +

+

+ A process inherits both uids from the process that invoked it, unless the program file it runs has its setuid permission bit set. In which case, the kernel then takes the effective uid from the file's owner instead, while the real uid remains inherited as before. A process therefore gets its effective uid in one of two ways: from the process that invoked it, or from the owner of a setuid program file. (Groups work the same way, with a real gid, an effective gid and a setgid bit, beside the supplementary groups, which are inherited unchanged.) +

+

+ By convention, the gate is the only program of Man_In_Grey that can optionally be given the setuid bit. When the gate is not setuid, it inherits its effective and real uids from the program that invoked it. When it is setuid, it inherits its real uid from the program that invoked it, and it inherits its effective uid from its file owner. Thus, the gate process has reliable information directly from the kernel on who invoked it, as that is its real uid. It also has reliable information directly from the kernel on who owned its executable file, as that becomes its effective uid. +

-

- An application making use of Man_In_Grey can bypass the orchestrator and call the composers and gate on its own. When this happens the gate's real ID will be that of the application. For a setuid gate, its effective uid still comes from its file owner. Such an application calls its composer functions however it likes, as many to a module as it likes, since it does no search for them. -

+

+ Due to this mechanism the effective uid for a setuid gate program can be different than the effective uid of the program that invoked it. In the chain of events of program A running and then invoking the gate, the effective uid in that thread of execution will start as the effective uid for program A, and then the effective uid will change to match the uid of the gate executable file owner. We can say that the effective uid change from A to B, where A is the invoking programs effective uid, an B is the owner of the gate executable file. +

+ -

- It is possible that the application is design such that the gate executable file does not have its setuid bit set, or that it does have its setuid set but the gate owner is the same as that of the orchestrator or that of the direct calling application. In such a case, the execution thread will keep the same real and effective uids the entire time it runs. In this mode the Man_In_Grey can not achieve anything the application could not have achieved on its own, but it still might be a convenient expression of the desired functionality. -

+ + Instruction language +

+ An instruction language is defined by the application developer and is built into the application. On the A side of the account divide, the composer writes the language by calling functions on the journal interface, one interface function per instruction. On the B account side of the divide, the guard checks the journal for correct syntax and that other constraints are met. +

+

+ The instruction language is not specific to Man_In_Grey. An application that mounts home directories has a language of mount and unmount; one that manages accounts has a language for making and deleting them. Each gate starts the guard and the interpreter of one instruction language, and they refuse a journal written in another language. These coherency checks are due to the journal carrying the name of its language, and due to syntax checking of the constituent instructions passing. +

+

+ A language can be made as narrow as its application. The narrower it is, the less a journal can say, and the less the guard has to rule out. The example language, , can name no file at all: what it writes, and where, is partially compiled in, and partially derived from the name of the invoking user account. +

+

+ Narrowness matters most for content. Constraints on where a file goes, and with what owner and permission, do not make the file safe when account A writes every byte of it. A configuration file is read by a program, often one started by root, and what the file says is what that program does; unbound.conf, for one, can name a Python script for the daemon to load. A language that lets account A write such a file freely gives account A much of the power of the program that reads it, however tightly its constraints fix the destination. The safe design is a language narrow enough that every journal it can express is safe: its interpreter writes the file, and account A supplies only values the language has a place for, as in the example. +

+ - - Gate -

- The gate is compiled because Linux ignores the setuid bit on a script started with #!. Given no arguments, the gate prints its usage. Its command flags reports the gate's real and effective uid and gid with their names, whether they differ, the name of the gate's instruction language, and the paths of the guard and the interpreter. -

- - > /usr/local/lib/Man_In_Grey/Man_In_Grey_gate/Man_In_Grey_emplace_bio_gate flags - real.uid=2006 - real.user_name=Thomas - real.gid=2006 - real.group_name=Thomas - effective.uid=996 - effective.user_name=http - effective.gid=995 - effective.group_name=http - uid_differ=1 - gid_differ=1 - language=emplace_bio - guard.path=/usr/local/lib/Man_In_Grey/Man_In_Grey/guard_emplace_bio.py - interpreter.path=/usr/local/lib/Man_In_Grey/Man_In_Grey/interpreter_emplace_bio.py - -

- Here Thomas asks the example language's gate, , installed setuid to the web server's account http: the real ids are his, and the effective ids are http's. -

+ + Data instance -

- Th admit command takes the journal on standard input, with the option check_only. When the gate is asked to admit a journal, it: -

- -
    -
  1. opens /dev/null on any of descriptors 0, 1 and 2 the invoking program left closed, and closes every descriptor above 2, so nothing the invoking program opened reaches the guard or the interpreter;
    2. -
  2. raises each resource limit that could stop the guard or the interpreter partway, file size and CPU time to unlimited, address space and data size to 1 GiB, stack size to 8 MiB, and open files to 64, as far as the hard limit allows, or past it when account B is root; and refuses when one stays too low;
    3. -
  3. finds the guard and the interpreter at paths fixed when the gate is compiled, relative to the gate itself, so account A cannot name others;
    4. -
  4. refuses unless the guard and the interpreter, and every directory above them, are owned by root or by account B, and writable by no other account;
    5. -
  5. clears the environment, setting only PATH and LANG, sets the file mode mask to 077, marks the process not dumpable, and changes directory to /;
    6. -
  6. records its real ids, account A's, in MIG_REAL_UID, MIG_REAL_GID and MIG_REAL_USER_NAME;
    7. -
  7. reads the journal from its standard input, up to 16 MiB;
    8. -
  8. starts /usr/bin/python3 -E -s -B on the guard, with the journal on its standard input, and goes on only when the guard approves the journal;
    9. -
  9. starts the interpreter the same way, with the same journal.
    10. -
-

- The guard and the interpreter, before they import anything, each check that every module they load, the guard program among them, is owned by root or by account B, and writable by no other account. A module runs code when it is imported, so the check comes first. -

-

- These checks are made on every run, whether or not the gate is setuid, and whoever account A is. A check that can be got around by other means still catches mistakes, such as a group-writable directory or an interpreter run from the wrong tree. When accounts A and B are the same, account B is the person's own account, so his own files pass. -

-

- The constraints, not the gate, decide which accounts can give a journal. The gate decides only whether the guard and the interpreter it would start can be trusted, and whether the guard approved the journal. -

-

- A gate that is not setuid keeps the uids of the program that invoked it, so accounts A and B are normally the same, and the guard still applies. A gate that is not setuid is the convenient way to use Man_In_Grey on files the person owns, and the way to prototype an instruction language before making a gate setuid for it. -

- - One gate per instruction language + + Journal +

+ A journal is a CBOR map of four entries: +

+ + + The version of the journal's form, now 3. A guard or interpreter refuses a journal of another version. + + + The name of the instruction language the journal is written in, such as emplace_bio. A guard and an interpreter refuse a journal in a language other than their own. + + + When, on which host and by which account the journal was composed, the composer directory, and the composers that ran, in order. + + + The instructions, in the order the composers placed them. + +

- Man_In_Grey's general gate is the library module Gate.lib.c, whose function Man_In_Grey_gate·Gate·run takes the name of the instruction language, the guard's path and the interpreter's path, and the command line. An instruction language's gate is a *.CLI.c of three lines that calls it with the three fixed. The gate of the example language: + Each instruction is a map of three entries: name, which instruction it is; argument, a map holding all of the instruction's arguments, each keyed by argument name; and composer, the composer that placed it. Man_In_Grey's orchestrator records there the path of the composer's file, relative to the composer directory; an application that places instructions itself records what it chooses. The first four instructions of the journal in , decoded, and written in JSON notation:

- #include "Gate.lib.c" - - int main(int argc ,char **argv){ - return Man_In_Grey_gate·Gate·run("emplace_bio" ,"../Man_In_Grey/guard_emplace_bio.py" - ,"../Man_In_Grey/interpreter_emplace_bio.py" ,argc ,argv); - } + {"name": "display_name", "argument": {"text": "Thomas"}, "composer": "bio.py"} + {"name": "paragraph", "argument": {}, "composer": "bio.py"} + {"name": "text", "argument": {"content": "I write ", "style": []}, "composer": "bio.py"} + {"name": "text", "argument": {"content": "software", "style": ["emphasis"]}, "composer": "bio.py"}

- The general gate is curried, with its first three arguments supplied when the gate is compiled. Whoever invokes a gate can choose neither program it runs; if he could, he could give it a guard that approves everything. The language name holds no space and no control character, and the gate refuses to run when it does. + An instruction that takes no arguments, such as paragraph, has an empty argument map. Arguments are given by name rather than by position, so the guard's wellformed check can require exactly the arguments an instruction takes: a text instruction carrying a third argument is refused, whatever that argument says.

- - - Output rule

- Every line the guard and the interpreter write is copied to the person, marked guard: or interpreter:, and to the system log under the name Man_In_Grey_gate, beside the gate's own lines, marked gate:. The gate logs each journal's course itself, whatever the guard and the interpreter write: received, with account A, account B and the journal's size; then approved or refused; then interpreting; then interpreted or failed. A line breaks the gate's rules when it is not UTF-8, or holds a control character (C0, DEL or C1), or is longer than 4096 bytes, or is one line more than 2000; the gate then stops the program and refuses the journal. Unicode is otherwise welcome. The guard writes any control character it quotes as \u{XXXX}, and the example language's wellformed check refuses any text that holds one. + An argument that is a symbol is the map {"symbol": <index>}, where the index locates the instruction that produces the value. In the account language of , the second instruction names the result of the first:

+ + {"name": "make_account", "argument": {"name": "Thomas·www"}, "composer": "www.py"} + {"name": "add_to_group", "argument": {"account": {"symbol": 0}, "group": "http"}, "composer": "www.py"} + +

+ Man_In_Grey's orchestrator runs the composers one after another into a single journal. Before it calls each composer's compose, it records that composer's path, relative to the composer directory, and every instruction placed during the call carries it. A journal composed from a directory of composers therefore shows which composer placed each instruction, and print shows it at the end of each line, which helps in finding the composer that placed a wrong one. The composer entry, like meta, is a note, not evidence: account A writes the whole journal, and could write anything there, so the guard and the interpreter never base a decision on either. +

+ + Symbol +

+ A composer writes instructions, but it does not run them. When an instruction would produce a result when run, as for example an instruction that makes an account and returns its uid, the result does not exist yet at the time the composer runs. Hence, when an instruction is entered into the journal via the journal interface, the interface returns a symbol placeholder. The symbol is then used as an argument by the composer when it enters instructions that are given said result as an argument. In the current implementation a symbol is simply the index into the journal that locates an instruction. Thus, with the current implementation each instruction can have at most one result. +

+ + account = journal_iface.make_account("Thomas·www") + journal_iface.add_to_group(account ,"http") + +

+ In this example account is a result symbol. The value of account will be 0, i.e. the index into the journal of the make_account instruction. The two instructions are of a language an application that manages accounts would define; the example language in has no instruction that produces a result. +

+ - - Least privilege, planned + + + + Program + + + Orchestrator

- A setuid gate owned by root gives the interpreter every one of root's rights. Root's rights are a set of about forty separate capabilities, among them CAP_DAC_OVERRIDE, to ignore file permissions; CAP_CHOWN, to change owners; CAP_SYS_ADMIN, to mount; and CAP_SETUID, to become another uid. The design is to give each such gate only the capabilities its instruction language needs. + The orchestrator is a utility program provided with Man_In_Grey. The orchestrator calls one or more composer programs, then sends the resulting journal to a gate program. Like all processes, when the orchestrator program runs, it has a real and effective uid. When the orchestrator is run from a shell, these are both inherited from the shell, and are typically pointing to the login user. In any case, the composers that it invokes will then run with the same effective and real uids as the orchestrator. When the gate executable file has its setuid bit set, when the gate is invoke by the orchestrator, the gate will inherit its real uid from the orchestrator, and will take its effective uid from the gate's executable file owner.

+

- setcap stores chosen capabilities in a program file's extended attributes. A process running that file holds them while its real and effective uid stay account A's. Capabilities are normally lost when a program execs one whose file holds none, as the gate does when it starts Python; the gate keeps them by raising them as ambient capabilities first, which survive the exec. A gate for a language that places files owned by other accounts would then be able to write files and change owners, and nothing else. The gain is uneven: CAP_SYS_ADMIN, needed for mounting, is nearly root by itself. + The orchestrator finds the composers by file. Given a composer file, or a composer directory, it runs each file, and in each it calls one function, compose(prov ,journal_iface). To the orchestrator a composer is therefore a file: each composer is to be given a file of its own, and the file is to define exactly one function of that form. The file can define other functions as helpers of it, but the orchestrator calls none of them, and a second function meant as a composer is never run. Several composers are several files, and the order of the files in the composer directory, as describes, is the order they run in.

- - - Installation + +

+ An application making use of Man_In_Grey can bypass the orchestrator and call the composers and gate on its own. When this happens the gate's real ID will be that of the application. For a setuid gate, its effective uid still comes from its file owner. Such an application calls its composer functions however it likes, as many to a module as it likes, since it does no search for them. +

+

- A setuid gate and everything its guard and interpreter load are to be owned by root or by account B, in directories no other account can write, and the gate and the interpreter check this. A Harmony consumer/ directory is owned by the person who promoted into it, so a setuid gate there refuses to run, and so does root running the gate there. Installing an instruction language's gate, guard and interpreter is a step of its own, done by root, or, when account B is not root, by root or by account B. The steps are in . + It is possible that the application is design such that the gate executable file does not have its setuid bit set, or that it does have its setuid set but the gate owner is the same as that of the orchestrator or that of the direct calling application. In such a case, the execution thread will keep the same real and effective uids the entire time it runs. In this mode the Man_In_Grey can not achieve anything the application could not have achieved on its own, but it still might be a convenient expression of the desired functionality.

- - - Guard -

- Accounts exist to limit what programs can do. The guard decides, before anything runs with the effective uid of account B, whether the work account A asks for is allowed: it reviews the journal and checks it against a set of constraints, and approves the journal only when every constraint is met. -

-

- The kernel tells the gate which account invoked it, as the real uid, and the gate passes it on, so the guard knows it also. The kernel does not say which program invoked the gate. As the guard invocation is compiled into the gate, the guard can know the provenance of the journal from the point it was given to the gate, but not before that. -

-

- Two checks are needed by nearly every guard, whatever its instruction language. The first is that the journal is well formed: that it decodes, names only instructions of its language, and gives each instruction the arguments it takes, of the right kinds. This check carries knowledge of the instruction syntax, so it belongs to the instruction language. The second is who account A is. The gate's real uid is account A's, and its real gid and supplementary groups are those it inherited from the invoking program, since the setuid and setgid bits change only the effective ids. All three pass to the guard, which reads them from the kernel, so account A cannot misstate them. A guard can therefore allow a journal from the accounts it names, or from the members of a group, as its constraints decide. -

-

- The other checks a guard makes belong to its instruction language. The example language's four checks are in . -

-

- A guard's constraints are code. The guard is a Python program, written for one application, so its constraints are Python functions written at the top of the guard itself, where they go with it, and no language for expressing constraints is needed. Each is a constraint predicate, named in the manner of is_allowed_account(user_name) or is_allowed_open(directory ,name ,mode ,owner ,permission), and the guard refuses a journal when one does not answer True. A predicate can compare with a list, ask whether an account is in a group, or anything else Python can say. The predicates sit between the lines # constraints begin and # constraints end, so that install_gate can put in an administrator's and keep them when the guard is installed again. As promoted with Man_In_Grey, they refuse every account. -

-

- Some constraints recur from one guard to the next, and the library module Constraint.py holds them, for a guard's predicates to call: -

- - - The account is in the group by the group database: listed as a member in /etc/group, or having it as its primary group. - - - The gate's real gid or supplementary groups include the group. These are what the invoking program held, passed on by the kernel, so an account that joined the group after its session began does not have it yet, though is_group_member already says yes. - - - The path is the directory or lies within it, both absolute and in normal form. - - - The permission sets no bit the limit does not: 0o600 is within 0o644, and 0o4755, setuid, is within neither 0o644 nor 0o755. - - -

- The guard checks and imports its modules, Constraint.py among them, only after its predicates are defined, and calls the predicates only after that, so a predicate can call Constraint.is_group_member by name, though the import comes later in the file. Code at the top level of the constraints runs before the ownership check, so the constraints hold only definitions, and imports of the standard library at most. The interpreter imports the guard program, for what execution needs from its constraints. -

- - Verdict + + Gate

- A guard reads the journal on its standard input. Its standard error is for the person: one line per finding, as <tag>: <message>, the first two name: and version:, then such lines as check_passed: wellformed or constraint_broken: <what is wrong>. Its standard output is for the verdict alone. A guard approves a journal by writing exactly one line there, guard <language> check passed, with the language name the gate has compiled in, and exiting 0. The gate takes the journal as approved on that line and that status together, and on nothing else, and only then admits it to the interpreter; a guard that refuses exits 1, and one that cannot check exits 2. + The gate is compiled because Linux ignores the setuid bit on a script started with #!. Given no arguments, the gate prints its usage. Its command flags reports the gate's real and effective uid and gid with their names, whether they differ, the name of the gate's instruction language, and the paths of the guard and the interpreter.

+ + > /usr/local/lib/Man_In_Grey/Man_In_Grey_gate/Man_In_Grey_emplace_bio_gate flags + real.uid=2006 + real.user_name=Thomas + real.gid=2006 + real.group_name=Thomas + effective.uid=996 + effective.user_name=http + effective.gid=995 + effective.group_name=http + uid_differ=1 + gid_differ=1 + language=emplace_bio + guard.path=/usr/local/lib/Man_In_Grey/Man_In_Grey/guard_emplace_bio.py + interpreter.path=/usr/local/lib/Man_In_Grey/Man_In_Grey/interpreter_emplace_bio.py +

- The verdict travels out of band from the findings. A finding quotes the journal, a file name for instance, and goes to standard error, so nothing in a journal can put a line on standard output. A crash cannot approve a journal either: an uncaught Python exception exits 1, and a guard that dies leaves no verdict. + Here Thomas asks the example language's gate, , installed setuid to the web server's account http: the real ids are his, and the effective ids are http's.

- - - - Interpreter -

- The gate starts the interpreter only after the guard has approved the journal, with the effective uid of account B and the same journal on its standard input. Generally the interpreter does not check the constraints as that is the guard's work, but some checks will naturally occur as part of interpretation. Where useful the guard program module can be included so as to pull in the helper functions. -

-

- The gate logs when a journal is received, approved, and interpreted. The interpreter's exit status is 0 when it finished the journal, 1 when it stopped partway, and 2 when the journal could not be read or is not well formed. The interpreter writes to standard output, as <tag>: <message>, the highlights of what it does, as its developer chooses them. -

-

- Execution stops at the first error. What the interpreter did before then stays done, except what its instruction language undoes; for the example language, see . Playing a journal as a transaction is a possible future feature; see . -

- +

+ Th admit command takes the journal on standard input, with the option check_only. When the gate is asked to admit a journal, it: +

- - Instruction language -

- An instruction language is defined by the application developer and is built into the application. On the A side of the account divide, the composer writes the language by calling functions on the journal interface, one interface function per instruction. On the B account side of the divide, the guard checks the journal for correct syntax and that other constraints are met. -

-

- The instruction language is not specific to Man_In_Grey. An application that mounts home directories has a language of mount and unmount; one that manages accounts has a language for making and deleting them. Each gate starts the guard and the interpreter of one instruction language, and they refuse a journal written in another language. These coherency checks are due to the journal carrying the name of its language, and due to syntax checking of the constituent instructions passing. -

-

- A language can be made as narrow as its application. The narrower it is, the less a journal can say, and the less the guard has to rule out. The example language, , can name no file at all: what it writes, and where, is partially compiled in, and partially derived from the name of the invoking user account. -

-

- Narrowness matters most for content. Constraints on where a file goes, and with what owner and permission, do not make the file safe when account A writes every byte of it. A configuration file is read by a program, often one started by root, and what the file says is what that program does; unbound.conf, for one, can name a Python script for the daemon to load. A language that lets account A write such a file freely gives account A much of the power of the program that reads it, however tightly its constraints fix the destination. The safe design is a language narrow enough that every journal it can express is safe: its interpreter writes the file, and account A supplies only values the language has a place for, as in the example. -

- +
    +
  1. opens /dev/null on any of descriptors 0, 1 and 2 the invoking program left closed, and closes every descriptor above 2, so nothing the invoking program opened reaches the guard or the interpreter;
    2. +
  2. raises each resource limit that could stop the guard or the interpreter partway, file size and CPU time to unlimited, address space and data size to 1 GiB, stack size to 8 MiB, and open files to 64, as far as the hard limit allows, or past it when account B is root; and refuses when one stays too low;
    3. +
  3. finds the guard and the interpreter at paths fixed when the gate is compiled, relative to the gate itself, so account A cannot name others;
    4. +
  4. refuses unless the guard and the interpreter, and every directory above them, are owned by root or by account B, and writable by no other account;
    5. +
  5. clears the environment, setting only PATH and LANG, sets the file mode mask to 077, marks the process not dumpable, and changes directory to /;
    6. +
  6. records its real ids, account A's, in MIG_REAL_UID, MIG_REAL_GID and MIG_REAL_USER_NAME;
    7. +
  7. reads the journal from its standard input, up to 16 MiB;
    8. +
  8. starts /usr/bin/python3 -E -s -B on the guard, with the journal on its standard input, and goes on only when the guard approves the journal;
    9. +
  9. starts the interpreter the same way, with the same journal.
    10. +
+

+ The guard and the interpreter, before they import anything, each check that every module they load, the guard program among them, is owned by root or by account B, and writable by no other account. A module runs code when it is imported, so the check comes first. +

+

+ These checks are made on every run, whether or not the gate is setuid, and whoever account A is. A check that can be got around by other means still catches mistakes, such as a group-writable directory or an interpreter run from the wrong tree. When accounts A and B are the same, account B is the person's own account, so his own files pass. +

+

+ The constraints, not the gate, decide which accounts can give a journal. The gate decides only whether the guard and the interpreter it would start can be trusted, and whether the guard approved the journal. +

+

+ A gate that is not setuid keeps the uids of the program that invoked it, so accounts A and B are normally the same, and the guard still applies. A gate that is not setuid is the convenient way to use Man_In_Grey on files the person owns, and the way to prototype an instruction language before making a gate setuid for it. +

+ + One gate per instruction language +

+ Man_In_Grey's general gate is the library module Gate.lib.c, whose function Man_In_Grey_gate·Gate·run takes the name of the instruction language, the guard's path and the interpreter's path, and the command line. An instruction language's gate is a *.CLI.c of three lines that calls it with the three fixed. The gate of the example language: +

+ + #include "Gate.lib.c" - - Journal -

- A journal is a CBOR map of four entries: -

- - - The version of the journal's form, now 3. A guard or interpreter refuses a journal of another version. - - - The name of the instruction language the journal is written in, such as emplace_bio. A guard and an interpreter refuse a journal in a language other than their own. - - - When, on which host and by which account the journal was composed, the composer directory, and the composers that ran, in order. - - - The instructions, in the order the composers placed them. - - -

- Each instruction is a map of three entries: name, which instruction it is; argument, a map holding all of the instruction's arguments, each keyed by argument name; and composer, the composer that placed it. Man_In_Grey's orchestrator records there the path of the composer's file, relative to the composer directory; an application that places instructions itself records what it chooses. The first four instructions of the journal in , decoded, and written in JSON notation: -

- - {"name": "display_name", "argument": {"text": "Thomas"}, "composer": "bio.py"} - {"name": "paragraph", "argument": {}, "composer": "bio.py"} - {"name": "text", "argument": {"content": "I write ", "style": []}, "composer": "bio.py"} - {"name": "text", "argument": {"content": "software", "style": ["emphasis"]}, "composer": "bio.py"} - -

- An instruction that takes no arguments, such as paragraph, has an empty argument map. Arguments are given by name rather than by position, so the guard's wellformed check can require exactly the arguments an instruction takes: a text instruction carrying a third argument is refused, whatever that argument says. -

-

- An argument that is a symbol is the map {"symbol": <index>}, where the index locates the instruction that produces the value. In the account language of , the second instruction names the result of the first: -

- - {"name": "make_account", "argument": {"name": "Thomas·www"}, "composer": "www.py"} - {"name": "add_to_group", "argument": {"account": {"symbol": 0}, "group": "http"}, "composer": "www.py"} - -

- Man_In_Grey's orchestrator runs the composers one after another into a single journal. Before it calls each composer's compose, it records that composer's path, relative to the composer directory, and every instruction placed during the call carries it. A journal composed from a directory of composers therefore shows which composer placed each instruction, and print shows it at the end of each line, which helps in finding the composer that placed a wrong one. The composer entry, like meta, is a note, not evidence: account A writes the whole journal, and could write anything there, so the guard and the interpreter never base a decision on either. -

- + int main(int argc ,char **argv){ + return Man_In_Grey_gate·Gate·run("emplace_bio" ,"../Man_In_Grey/guard_emplace_bio.py" + ,"../Man_In_Grey/interpreter_emplace_bio.py" ,argc ,argv); + } + +

+ The general gate is curried, with its first three arguments supplied when the gate is compiled. Whoever invokes a gate can choose neither program it runs; if he could, he could give it a guard that approves everything. The language name holds no space and no control character, and the gate refuses to run when it does. +

+ + + Output rule +

+ Every line the guard and the interpreter write is copied to the person, marked guard: or interpreter:, and to the system log under the name Man_In_Grey_gate, beside the gate's own lines, marked gate:. The gate logs each journal's course itself, whatever the guard and the interpreter write: received, with account A, account B and the journal's size; then approved or refused; then interpreting; then interpreted or failed. A line breaks the gate's rules when it is not UTF-8, or holds a control character (C0, DEL or C1), or is longer than 4096 bytes, or is one line more than 2000; the gate then stops the program and refuses the journal. Unicode is otherwise welcome. The guard writes any control character it quotes as \u{XXXX}, and the example language's wellformed check refuses any text that holds one. +

+ + + Transport +

+ A journal reaches its interpreter by starting the interpreter's gate with the journal on standard input. Since a journal is data, it could travel other ways, such as over a Unix domain socket to an interpreter already running, which would learn account A through SO_PEERCRED. Man_In_Grey does not do this. It is the mechanism a program that receives requests is built with, not such a program itself. +

+ + - - Transport -

- A journal reaches its interpreter by starting the interpreter's gate with the journal on standard input. Since a journal is data, it could travel other ways, such as over a Unix domain socket to an interpreter already running, which would learn account A through SO_PEERCRED. Man_In_Grey does not do this. It is the mechanism a program that receives requests is built with, not such a program itself. -

+ + Guard +

+ Accounts exist to limit what programs can do. The guard decides, before anything runs with the effective uid of account B, whether the work account A asks for is allowed: it reviews the journal and checks it against a set of constraints, and approves the journal only when every constraint is met. +

+

+ The kernel tells the gate which account invoked it, as the real uid, and the gate passes it on, so the guard knows it also. The kernel does not say which program invoked the gate. As the guard invocation is compiled into the gate, the guard can know the provenance of the journal from the point it was given to the gate, but not before that. +

+

+ Two checks are needed by nearly every guard, whatever its instruction language. The first is that the journal is well formed: that it decodes, names only instructions of its language, and gives each instruction the arguments it takes, of the right kinds. This check carries knowledge of the instruction syntax, so it belongs to the instruction language. The second is who account A is. The gate's real uid is account A's, and its real gid and supplementary groups are those it inherited from the invoking program, since the setuid and setgid bits change only the effective ids. All three pass to the guard, which reads them from the kernel, so account A cannot misstate them. A guard can therefore allow a journal from the accounts it names, or from the members of a group, as its constraints decide. +

+

+ The other checks a guard makes belong to its instruction language. The example language's four checks are in . +

+ + Constraint predicate +

+ A guard's constraints are code. The guard is a Python program, written for one application, so its constraints are Python functions written at the top of the guard itself, where they go with it, and no language for expressing constraints is needed. Each is a constraint predicate, named in the manner of is_allowed_account(user_name) or is_allowed_open(directory ,name ,mode ,owner ,permission), and the guard refuses a journal when one does not answer True. A predicate can compare with a list, ask whether an account is in a group, or anything else Python can say. The predicates sit between the lines # constraints begin and # constraints end, so that install_gate can put in an administrator's and keep them when the guard is installed again. As promoted with Man_In_Grey, they refuse every account. +

+

+ Some constraints recur from one guard to the next, and the library module Constraint.py holds them, for a guard's predicates to call: +

+ + + The account is in the group by the group database: listed as a member in /etc/group, or having it as its primary group. + + + The gate's real gid or supplementary groups include the group. These are what the invoking program held, passed on by the kernel, so an account that joined the group after its session began does not have it yet, though is_group_member already says yes. + + + The path is the directory or lies within it, both absolute and in normal form. + + + The permission sets no bit the limit does not: 0o600 is within 0o644, and 0o4755, setuid, is within neither 0o644 nor 0o755. + + +

+ The guard checks and imports its modules, Constraint.py among them, only after its predicates are defined, and calls the predicates only after that, so a predicate can call Constraint.is_group_member by name, though the import comes later in the file. Code at the top level of the constraints runs before the ownership check, so the constraints hold only definitions, and imports of the standard library at most. The interpreter imports the guard program, for what execution needs from its constraints. +

+ + + Verdict +

+ A guard reads the journal on its standard input. Its standard error is for the person: one line per finding, as <tag>: <message>, the first two name: and version:, then such lines as check_passed: wellformed or constraint_broken: <what is wrong>. Its standard output is for the verdict alone. A guard approves a journal by writing exactly one line there, guard <language> check passed, with the language name the gate has compiled in, and exiting 0. The gate takes the journal as approved on that line and that status together, and on nothing else, and only then admits it to the interpreter; a guard that refuses exits 1, and one that cannot check exits 2. +

+

+ The verdict travels out of band from the findings. A finding quotes the journal, a file name for instance, and goes to standard error, so nothing in a journal can put a line on standard output. A crash cannot approve a journal either: an uncaught Python exception exits 1, and a guard that dies leaves no verdict. +

+ + + + + Interpreter +

+ The gate starts the interpreter only after the guard has approved the journal, with the effective uid of account B and the same journal on its standard input. Generally the interpreter does not check the constraints as that is the guard's work, but some checks will naturally occur as part of interpretation. Where useful the guard program module can be included so as to pull in the helper functions. +

+

+ The gate logs when a journal is received, approved, and interpreted. The interpreter's exit status is 0 when it finished the journal, 1 when it stopped partway, and 2 when the journal could not be read or is not well formed. The interpreter writes to standard output, as <tag>: <message>, the highlights of what it does, as its developer chooses them. +

+

+ Execution stops at the first error. What the interpreter did before then stays done, except what its instruction language undoes; for the example language, see . Playing a journal as a transaction is a possible future feature; see . +

+ @@ -493,7 +491,10 @@ Installing a setuid gate

- A setuid gate is installed by root, with install_gate, which is promoted beside Man_In_Grey: + A setuid gate and everything its guard and interpreter load are to be owned by root or by account B, in directories no other account can write, and the gate, the guard and the interpreter check this on every run. A Harmony consumer/ directory is owned by the person who promoted into it, so a setuid gate there refuses to run, and so does root running the gate there. Installing an instruction language's gate, guard and interpreter is therefore a step of its own, done by root. +

+

+ The installation is done with install_gate, which is promoted beside Man_In_Grey:

sudo consumer/Man_In_Grey/install_gate install <gate> owner <account> into <directory> [constraints <file>] @@ -782,6 +783,15 @@ Possible future feature + + Least privilege +

+ A setuid gate owned by root gives the interpreter every one of root's rights. Root's rights are a set of about forty separate capabilities, among them CAP_DAC_OVERRIDE, to ignore file permissions; CAP_CHOWN, to change owners; CAP_SYS_ADMIN, to mount; and CAP_SETUID, to become another uid. The design is to give each such gate only the capabilities its instruction language needs. +

+

+ setcap stores chosen capabilities in a program file's extended attributes. A process running that file holds them while its real and effective uid stay account A's. Capabilities are normally lost when a program execs one whose file holds none, as the gate does when it starts Python; the gate keeps them by raising them as ambient capabilities first, which survive the exec. A gate for a language that places files owned by other accounts would then be able to write files and change owners, and nothing else. The gain is uneven: CAP_SYS_ADMIN, needed for mounting, is nearly root by itself. +

+ Namespace in place of index symbol