Aquinas

Mar 12, 2020

Aquinas is an interactive learning system that aims to teach computer programming and exploit development. Teachers define programming projects, and students complete the projects and submit their work using Git. Aquinas provides a website that lists the projects and provides a summary of each student’s progress.

A number of goals drove the design of Aquinas:

Allow for projects that involve network programming and exploit development.
Facilitate easy-to-define projects with a consistent specification language.
Ease reuse of projects across many programming languages.
Allow for high-quality assignment instructions.
Provide a web- and Git-based interface to students.
Provide for automated grading and student feedback.
Apply the principle of least privilege and use a type-safe language.

Aquinas dependencies

Building, configuring, and deploying Aquinas requires the following software:

make
GCC, including support for C++ (to build VMs)
A C library suitable for static linking
expect
qemu-system-x86
The Go programming language
The Perl programming language (to build VMs)
The jq JSON parser
Git
An ssh client
LaTeXML and TeX Live
The tidy HTML beautifier
The dig DNS resolver
The Hugo website generator
The wget HTTP utility (to build VMs)
which

Obtaining Aquinas

Download Aquinas using:

git clone --recurse-submodules https://www.flyn.org/git/aquinas

Building Aquinas

Building Aquinas can take a long time. If you prefer to install Aquinas using the binary VM images we provide, then download them from https://www.flyn.org/projects/Aquinas, and skip to the section titled “Configuring and deploying Aquinas.”

Quick check

Run “make deps all”.
Run “(sudo) ./build/httpd -dummy -root www/public/”.

You should now be able to browse to http://localhost/. The dynamic aspects of Aquinas will not work without a full installation, but you should be able to review most of Aquinas’ look and feel using this dummy mode.

Full build

Review aquinas-build.json to facilitate installing Aquinas at your site. The default values should be adequate in most cases.
Run “make deps all vms”. This will build some utilities and the Aquinas VMs.

Configuring and deploying Aquinas

Install your public SSH key the VMs by running “./aquinas-setup-ssh-developer DEVELOPER-HOME/.ssh/id_rsa.pub” with root privileges. (Mounting the VM disk images requires root privileges.)
Install each disk image (e.g., aquinas-git-alpine-x86-64.img) and each domain configuration (e.g., vm-aquinas-git.cfg) so that they can be run by your hypervisor. Edit each domain configuration to suit your needs. (Note that you will need to build a new VM around each disk image if not using Xen.)
Update your DHCP service to provide the correct IP address to each domain. Refer to each domain configuration for the host’s MAC address.
Update your DNS service to provide an appropriate A record for each domain. Refer to each domain configuration for the host’s name.
Start each configured VM.
Use SSH to sign in on each VM to edit /etc/aquinas/aquinas.json. It is likely you will need to modify “domain,” “logServer,” “emailRegex,” “emailRelay,” emailSender," and “emailSenderName.”
Install a certificate and private key in aquinas-www’s /etc/httpd directory, writing them to the files aquinas.cert and aquinas.key, respectively.
Configure syslog-ng on each VM. The /etc/hosts files on aquinas-user and aquinas-target must contain records for the syslog server (which accepts connections on TCP port 6514), as their firewall prohibits DNS queries.
Configure collectd on each VM. The /etc/hosts files on aquinas-user and aquinas-target must contain records for the collectd server (which accepts connections on UDP port 25826), as their firewall prohibits DNS queries.
Add a record for your target host to /etc/hosts on your user host; neither can make DNS requests, as their firewall prohibits DNS queries.
Add a record for your user host to /etc/hosts on your target host.
Add “server [IP of git host]” to /etc/ntpd.conf on www, user, and target.
Edit /etc/config/system on each VM. You might need to adjust the timezone, and you should set the NTP server to the IP address of aquinas-git host on all of the VMs except for aquinas-git. Note that the firewall rules will allow NTP queries from aquinas-user and aquinas-target only to aquinas-git, and these hosts can only reference aquinas-git by its IP address due to the firewall blocking DNS.
On your development computer, run “./aquinas-setup-ssh”.
On aquinas-www, run “sudo -u http aquinas-add-student test PASSWORD ‘Test Account’”. Ensure you select a strong password to replace PASSWORD.
On your development computer, run “./aquinas-add-teacher DEVELOPER-HOME/.ssh/id_rsa.pub”.
Push a projects repository to aquinas-git:/home/teacher/projects.
Push a records repository to aquinas-git:/home/teacher/records.
Push the HTML documents to aquinas-www using make all publish.
On your development computer and from the directory test/, run “./test-all.”

Writing a project

Writing a project is a matter of creating a machine-readable JSON file to define the project and a LaTeX (or Markdown) fragment to instruct students in how to complete the project.

Project definition

Here is the definition of a very simple project named unix. The absence of the checks keyword means that Aquinas will not grade this project. Because languages is set to none, Aquinas will generate no language-specific variants of this project. Perhaps this project could guide the student through an introduction to UNIX without requiring a graded deliverable.

{
        "name": "unix",
      "summary": "An introduction to Unix and the Bourne shell",
        "languages": [ "none" ]
}

Here is another language-agnostic project. This project, git, assumes the completion of unix. Aquinas will take this into account when ordering the list of projects presented to a student. This project provides a check (checks); running the command cat NOTES from the root of the student’s Git repository should print “In case of fire: git commit, git push, and leave the building!” to standard out. (I.e., the file NOTES should exist in the Git repository and it should contain “In case of fire: …”)

The value in the stdout field is this string, base64 encoded (but not depicted in its entirety here). The base64 encoding is to allow such values to contain binary data.

Aquinas will present the string defined in a check’s hint field as part of the feedback it provides upon grading a failed submission.

{
      "name": "git",
      "summary": "An introduction to the Git version control system",
      "languages": [
              "none"
      ],
      "prerequisites": [
              "unix"
      ],
      "checks": [
              {
                      "type": "basic",
                      "parameters": {
                              "command": "cat NOTES",
                              "stdin": null,
                              "stdout": "SW4gY2Fz...",
                              "stderr": null,
                              "exitCode": 0,
                              "hint": "Does your NOTES file contain the correct string?"
                      }
              }
      ]
}

Using a check of kind compare causes Aquinas to evaluate student work in a different way. With compare checks, Aquinas can reveal its test inputs without allowing the student to tailor his solution to a limited test plan. The idea is to use a generator to produce random input that is well-formed with respect to the project definition. Aquinas generates such input, which it provides both to the reference solution and the student submission. If the programs’ outputs match, then Aquinas deems the student submission correct. Otherwise, the student submission is incorrect. A compare check requires the definition of a reference solution along with a program that generates standard input data (genstdin) or a program that generates command-line arguments (gencmdargs). The following example demonstrates a compare check that generates standard input data.

{
      "kind": "compare",
      "parameters": {
              "command": "./project",
              "reference": "projectC.c",
              "genstdin": "generator-project.c"
      }
},

Assume the project processes non-negative integers, read from standard input. The following definition of generator-project.c generates such inputs.

#include <stdio.h>
#include <stdlib.h>
#include <sys/time.h>

int main(void)
{
        struct timeval tv;

        gettimeofday(&tv, NULL);
        srand((unsigned int)(tv.tv_sec * tv.tv_usec));
        printf("%d\n", rand());
}

The use of gencmdargs is similar. Aquinas assumes each line printed by this type of generator represents a command-line argument. Aquinas will compile and deploy generators and reference solutions that exist in a project’s directory and are referenced by a compare check.

A student may submit the following project in C or Python. In the case of C, the submission should contain hello.c, and this file should compile to a program that prints “Hello, world\n”. A Python submission should take the form of hello as an executable script (i.e., with shebang). As with the previous example, the value of stdout is base64 encoded to support binary data.

{
      "name": "hello",
      "summary": "Printing to the screen",
      "languages": [
              "C",
              "Python"
      ],
      "prerequisites": [
              "git"
      ],
      "checks": [
              {
                      "type": "basic",
                      "parameters": {
                              "command": "./hello",
                              "stdin": null,
                              "stdout": "SGVsbG8sIHdvcmxkIQo=",
                              "stderr": null,
                              "exitCode": 0
                      }
              }
      ]
}

The following network project installs a service, defined in network.go, on Aquinas’ target host. A correct solution will interact with this service as the project instructions prescribe to produce the output required by the project’s checks. The value of source minus its extension must match the value of name, and every project must bear a unique port. Note that Aquinas will replace TARGET with the target host’s name when performing this check.

{
      "name": "network",
      "summary": "Programming a TCP/IPv4 client",
      "languages": [
              "C",
              "Go",
              "Python"
      ],
      "prerequisites": [
              "hello",
              "variables"
      ],
      "checks": [
              {
                      "type": "basic",
                      "parameters": {
                              "command": "./network TARGET 1025",
                              "stdin": null,
                              "stdout": "...",
                              "stderr": null,
                              "exitCode": 0
                      }
              }
      ],
      "services": [
              {
                      "source": "service-network.go",
                      "port": 1025
              }
      ]
}

Adding the following within a particular service’s definition makes the service binary available for download.

        "publish_binary": true

A teacher can also specify flags in a service definition that Aquinas will pass to the compiler when building the service binary:

        "compiler_flags": "-fstack-protector"

When presenting lists of projects, Aquinas will make use of tags for organization. A set of tags augment the language categories:

       "tags": {
              "Exploitation": true
      }

Sometimes it might be useful to directly call functions in a project solution when testing. An altmain statement allows this. For example, if altmain is defined as true for C, Aquinas will compile the submitted program such that the function main2 in the teacher-defined file main2.c serves as the program’s main function.

{
      "name": "functions",
      "summary": "Abstraction and code reuse using functions",
      "languages": [
              "C",
              "Go",
              "Python"
      ],
      "prerequisites": [
              "hello",
              "variables"
      ],
      "altmain": {
              "C": true,
              "Go": true,
              "Python": true
      },
      "checks": [
              {
                      "type": "basic",
                      "parameters": {
                              "command": "./functions",
                              "stdin": null,
                              "stdout": "...",
                              "stderr": null,
                              "exitCode": 0
                      }
              }
      ]
}

Aquinas supports solution templates, which provide students with a starting point for their solution. In this example, the values of templates should correspond with template files for C, Go, and Python. These files must exists in the same Git repository as this description, and Aquinas will copy them to the students’ variables repositories. If the template value is a directory, then Aquinas will copy all of the files in that directory to the root of the student’s repository.

{
      "name": "variables",
      "summary": "Programming language variables and arithmetic operators",
      "languages": [
              "C",
              "Go",
              "Python"
      ],
      "prerequisites": [
              "hello"
      ],
      "checks": [
              {
                      "type": "basic",
                      "parameters": {
                              "command": "./variables",
                              "stdin": "...",
                              "stdout": "...",
                              "stderr": null,
                              "exitCode": 0
                      }
              },
              {
                      "type": "basic",
                      "parameters": {
                              "command": "./variables",
                              "stdin": "...",
                              "stdout": "...",
                              "stderr": null,
                              "exitCode": 0
                      }
              },
              {
                      "type": "basic",
                      "parameters": {
                              "command": "./variables",
                              "stdin": "...",
                              "stdout": "...",
                              "stderr": null,
                              "exitCode": 0
                      }
              }
      ],
      "templates": {
              "C": "template-variablesC.c",
              "Go": "template-variablesGo.go",
              "Python": "template-variablesPython"
      }
}

Aside from templates, Aquinas supports the following file-related specifications. Each of these name an array of strings:

files: Causes grader to place files in student's submission directory after cloning it, possibly overwriting what is already there
user_files: Places files in /usr/libexec/aquinas/files/PROJECT on aquinas-user, making them available to the grader
service_files: Places files in /usr/libexec/aquinas/services/PROJECT on aquinas-target, making them available to the target service
service_links: Set up a link on aquinas-target from the given path outside the service chroot to inside of the service chroot
service_chroot_programs: Copies files from outside the target service chroot to inside the target service chroot

Project instructions

Teachers write project instructions in the form of a LaTeX fragment, which Aquinas combines with a template before processing into a HTML document. It is a good practice to use \section* to provide three sections: Command (or Function) summary, Lesson, and Assignment. Aquinas will provide the prelude and epilog material; here it is sufficient to begin with the first \section*.

Aquinas provides the following LaTeX commands for use in a project’s instructions:

\cmd

Typeset the argument as a command.

\project

Typeset the argument as a project name.

\conf

Typeset the argument as a configuration file.

\file

Typeset the argument as a file name.

\dir

Typeset the argument as a directory name.

\fn

Typeset the argument as a function name.

\host

Typeset the argument as a host name.

\keypress

Typeset the argument as if it were a key to be pressed.

\unix

Typeset the work UNIX.

\shprompt

Typeset a Bourne shell prompt.

\cmddesc

Define a command within a LaTeX description list. Like \item, except Aquinas notes occurences of \cmddesc to produce a command reference page.

\fncdesc

Define a C function within a LaTeX description list. Like \item, except Aquinas notes occurences of \fncdesc to produce a C function reference page. Variants exist for other languages such as Go (\fngodesc) and Python (\fnpythondesc).

\ifC

If the language associated with the current project variant matches (here the C variant), then include the subsequent text up until the next \fi. Otherwise print nothing.

\ifshebang

If the language can make use of a shebang, then print the second argument. Otherwise print nothing.

\clone

Provide instructions on how to clone the current project using Git.

\submission

Print instructions on how to submit a project solution.

\submissionNoLanguage

Print instructions on how to submit a language-agnostic project solution.

Alternatively, a teacher can describe a project using Markdown.

The Aquinas VMs

aquinas-www: The HTTP server that allows users to read project assignments and view submission results.
aquinas-git: The Git server to which users make project submissions.
aquinas-user: The host that runs project submissions during the grading process.
aquinas-target: The host that runs network services with which user programs might interact.

System inputs

(unauthenticated) http://aquinas-www/landing.html: Allows a user to either log in or register.
(unauthenticated) http://aquinas-www/login.html: Accepts student email and password. Allows a student to log in to the web interface. Transitions state of HTTP session to authenticated.
(unauthenticated) http://aquinas-www/register.html: Accepts an email address. Allows a registering student to initiate the registration process. Sends an email to the registering student that allows him to complete the registration.
(unauthenticated) http://aquinas-www/register3.html: Accepts an email address, nonce, hashed token, and password. Allows a registering student to prove ownership of an email address and thus complete the registration process.
(authenticated) http://aquinas-www/index.html: Allows a student to select a project page.
(authenticated) http://aquinas-www/p.html, where p is a project: Allows a student to view information that describes project p.
ssh://s@aquinas-git/home/s/p, where s is a student and p is a project: Interact with student s's project p submission using Git/git-shell.
Git hook invokes grader, run as teacher, with s and p as its input.
ssh://t@aquinas-git/home/teacher/projects, where t is a teacher: Interact with the project definitions using Git/git-shell. Git hook invokes aquinas-initialize-projects, run as root.
ssh://t@aquinas-git/home/teacher/records, where t is a teacher: Interact with the project submission records using Git/git-shell.
ssh://root@\*: Allows developers shell access.

Sudo permissions

aquinas-git

All users can run grader as teacher
Teacher can run aquinas-initialize-projects as root
Http can run aquinas-add-student-slave as root
Http can run aquinas-get-ssh-authorized-keys as root
Http can run aquinas-deploy-key as root
Http can run aquinas-remove-student-slave as root

SSH keys

root@aquinas-git: generated by alpine-build
teacher@aquinas-git: generated by alpine-build
http@aquinas-www: generated by alpine-build
Developers: installed by hand
Teachers: installed by aquinas-add-teacher
Students: installed by ssh/ssh2.html

Permitted SSH connections

From	To	Installed by	Purpose
Developers	root@aquinas-git	alpine-build/manual	Development/administration
Developers	test@aquinas-git	test case	Pushing solutions during test
Teachers	teacher@aquinas-git	add-teacher	Project deployment
http@aquinas-www	http@aquinas-git	setup-ssh	Httpd uses to run httpsh: check for student check for SSH key add a new student deploy SSH key remove a student
Students	STUDENT@aquinas-git	ssh/ssh2.html	Commit submissions to Git
Developers	root@aquinas-www	alpine-build/manual	Development/administration
Teachers	teacher@aquinas-www	add-teacher	Updating HTML documents
teacher@aquinas-git	teacher@aquinas-www	setup-ssh	Used by grader to update records on aquinas-www
Developers	root@aquinas-user	alpine-build/manual	Development
teacher@aquinas-git	root@aquinas-user	setup-ssh	Used by initialize-project to pull host key and user key from aquinas-user (Cannot use test@, because test has shell set to buildrunsh) Also used by grader to place user-submitted code on aquinas-user
teacher@aquinas-git	teacher@aquinas-user	setup-ssh	Used grader to run reference solution on aquinas-user in the case of compare-type checks
root@aquinas-git	root@aquinas-user	setup-ssh	Add or remove user
root@aquinas-git	teacher@aquinas-user	setup-ssh	Compile network project services
teacher@aquinas-git	STUDENT@aquinas-user	add-student	Grader uses to run buildrunsh on user VM; Git hook runs as user, and uses sudo to run grader as teacher
root@aquinas-git	root@aquinas-target	setup-ssh	Deploy network project services

Component isolation

The design of Aquinas isolates its components to prevent student program from exfiltrating data available to them during the grading process. This prevents student knowledge of the checks that grade their submissions. Furthermore, student programs cannot interact beyond the aquinas-user host with the exception of allowed connections to aquinas-target.

Firewall rules

The host firewalls on aquinas-user and aquinas-target prohibit all outgoing connections with the exception of a connection to a syslog server (TCP port 6514). All interaction with these hosts is by way of incoming SSH connections or project-specific services. The aim of this is to prevent a user-written program from exfiltrating data from either host while executing for the purpose of grading.

Chroot jails

Services on aquinas-target run as the user nobody and within a chroot jail.

Aquinas administation

Manually fork a repository

The following assumes the student is using Aquinas’ native Git repository, rather than a third-party repository such as GitLab. If this is not the case, then you would need to provide more information in the JSON-encoded parameter.

aquinas-fork-project STUDENT@EXAMPLE.COM PROJECT '{"git-provider":"","git-path":"","git-username":"","git-token":""}' [LANG]

Force the grading of a project

root@aquinas-git> aquinas-enqueue /usr/sbin/grader STUDENT@EXAMPLE.COM PROJECTLANG

Force the grading of a project directly, without using the queuing system

root@aquinas-git> scp -r /home/teacher/workdir/students/STUDENT@EXAMPLE.COM/helloC/ root@aquinas-user.EXAMPLE.COM:/home/STUDENT@EXAMPLE.COM/helloC/
root@aquinas-git> ssh root@aquinas-user.EXAMPLE.COM chown -R STUDENT_at_EXAMPLE_dot_COM:STUDENT_at_EXAMPLE_dot_COM /home/STUDENT@EXAMPLE.COM/helloC
root@aquinas-git> ( echo \"C\"; cat /home/teacher/workdir/projects/hello/description.json ) | sudo -u teacher ssh -T STUDENT_at_EXAMPLE_dot_COM@aquinas-user.EXAMPLE.COM

Rename a user

Note the student’s alias.
Backup the student OLD’s home directory at /home/OLD@EXAMPLE.COM.
On aquinas-www, run sudo -u http aquinas-remove-student OLD@EXAMPLE.COM.
On aquinas-www, run sudo -u http aquinas-add-student NEW@EXAMPLE.COM PASSWORD.
Install SSH key from backup.
Restore student’s alias.
For each repository in the backup, git clone the repository to a temporary location, and from that location run git push repo=NEW_AT_EXAMPLE_DOT_COM@aquinas-git.DOMAIN:/home/NEW@EXAMPLE.COM/PROJECT --all --force.

Mark a user as a teacher

root@aquinas-www> touch /etc/httpd/accounts/USER/teacher
root@aquinas-www> chown http:www-data /etc/httpd/accounts/USER/teacher

Courses as Code: The Aquinas Learning System

W. Michael Petullo

Downloads

The Aquinas project is also available as a Git repository. To clone the repository, execute

git clone --recurse-submodules https://www.flyn.org/git/aquinas