Необходимо перевести следующий профиль AppArmor (сделанный для Nginx) на язык Promela для последующей его верификации в программе SPIN:

#include <tunables/global>
/usr/sbin/nginx {
#include <abstractions/base>
#include <abstractions/dovecot-common>
#include <abstractions/nameservice>
#include <abstractions/nis>
#include <abstractions/openssl>
#include <abstractions/postfix-common>
capability dac_override,
/usr/sbin/nginx mr,
/var/log/nginx/access.log w,
/var/log/nginx/error.log w,
/var/www/html/* r,
owner /etc/nginx/* r,
owner /etc/nginx/conf.d/ r,
owner /etc/nginx/modules-enabled/ r,
owner /etc/nginx/sites-available/* r,
owner /etc/nginx/sites-enabled/* r,
owner /proc/sys/kernel/random/boot_id r,
owner /run/nginx.pid rw,
owner /usr/share/nginx/modules-available/* r,
}

В рамках работы не требуется проводить верификацию, только произвести перевод