Использование Ваучера Лиспекса

Подготовьте Native и новый рабочий каталог. Команды используют POSIX-оболочку, например Git Bash в Windows. В этом упражнении вы выполняете роли издателя и получателя на одной машине. При раздельной работе получатель независимо проверяет открытый ключ издателя, идентификатор точного исполняемого файла и исходник правила.

Подготовьте правило и вход

Сохраните всю программу как print-handoff.lspx. Приложение проверяет окончательный файл и передаёт четыре логических результата в согласованном порядке.

LISPEX

(define параметры-печати-верны?
  (and (car input)
       (car (cdr input))
       (car (cdr (cdr input)))
       (car (cdr (cdr (cdr input))))))

(if параметры-печати-верны?
    (decision-approve)
    (decision-deny))

Сохраните input.checked.json в точности как показано ниже. Сохраните оба файла в UTF-8 без BOM, с окончаниями строк LF и одним завершающим переводом строки. Сохраните отступы входа в два пробела.

JSON

{
  "input": "csk.checked-input/v1",
  "value": [
    true,
    true,
    true,
    true,
    "edition-final"
  ]
}

Первые четыре значения означают успешную проверку формата страницы, полей, встроенных шрифтов и числа страниц в указанном порядке. Пятое обозначает согласованную сторонами редакцию окончательного файла. Приложение связывает её с точным производственным файлом и хранит его. Правило читает четыре логических значения, а подпись связывает все пять значений ввода. Результат примера равен approve. csk.checked-profile/v1 обозначает используемый профиль языка.

Подготовьте ключ подписи

Создайте локальную пару ключей Ed25519 для упражнения и проверьте открытый ключ.

lispex key generate --out-dir issuer-key
lispex key inspect --public-key issuer-key/public.spki.der

Обе команды завершаются с кодом 0. Генерация выводит JSON с "status": "generated" и создаёт issuer-key/private.pkcs8.der и issuer-key/public.spki.der. Проверка выводит JSON с "status": "valid". Издатель подписывает записи закрытым ключом. Получатель выбирает открытый ключ для политики, а закрытый ключ остаётся у издателя.

Выведите идентификаторы выбранных файлов. Замените /absolute/path/to/lispex абсолютным путём к вашему исполняемому файлу Native. В Windows подойдёт путь вида D:/tools/lispex.exe.

lispex vouch key-id --public-key issuer-key/public.spki.der
lispex vouch engine-id --executable /absolute/path/to/lispex
lispex vouch source-id --source print-handoff.lspx
lispex vouch input-id --input input.checked.json

Каждая команда выводит один идентификатор и завершается с кодом 0. key-id зависит от созданного ключа. engine-id начинается с sha256: и идентифицирует точный исполняемый файл. Проверьте это значение перед включением в политику. Для приведённых исходника и входа последние две команды выводят следующие значения.

4f1e43c37d82fb44da9bfd341e3471151d7ff3af4a6900e25a2df96ae23ffeb5
9e1f420be1fc34992b76a0b1d88ea20e72243f6f4ca5a80210298e1693d006cf

1. Создайте политику получателя

Замените заполнитель в ENGINE_ID полным проверенным выводом engine-id, включая sha256:. Укажите открытый ключ и исходник, которые вы проверили.

ENGINE_ID="sha256:<reviewed-native-engine-digest>"
lispex vouch policy create \
  --public-key issuer-key/public.spki.der \
  --engine-sha256 "$ENGINE_ID" \
  --source print-handoff.lspx \
  --out policy.json

lispex vouch policy check --trust-policy policy.json

Создание записывает policy.json. Обе команды завершаются с кодом 0 без вывода. Политика хранит допустимые ключ, движок, профиль языка и идентификатор исходника в едином установленном байтовом формате. Этот шаг подготавливает настройки доверия. Далее издатель подписывает запись выполнения.

2. Выдайте подписанную запись

В ISSUER_KEY_URI укажите pkcs8-file:// и абсолютный путь к закрытому ключу. Путь Linux или macOS начинается с pkcs8-file:///. В Windows используйте значение вида pkcs8-file://D:/vouch-example/issuer-key/private.pkcs8.der. Замените путь ниже перед запуском.

ISSUER_KEY_URI="pkcs8-file:///absolute/path/to/issuer-key/private.pkcs8.der"
lispex vouch issue \
  --source print-handoff.lspx \
  --input input.checked.json \
  --profile csk.checked-profile/v1 \
  --key-handle "$ISSUER_KEY_URI" \
  --out-dir issued \
  --emit-bundle

Команда завершается с кодом 0 без вывода. Native выполняет исходник интерпретатором Лиспекса и интерпретатором Meaning и подписывает обе полные записи выполнения. Интерпретатор Лиспекса читает исходник, нормализует его в основные формы CoreExpr и вычисляет их. Meaning вычисляет представление, полученное из этого исходника.

Команда создаёт следующие файлы в issued/. Для каждой выдачи выбирайте новый выходной каталог.

Файл	Содержимое
`issue-report.json`	Результат выдачи с `"status": "issued-native"` и `"primary_error": null`
`payload.json`	Исходник, вход, профиль, движок, результат и полный контекст выполнения
`envelope.dsse.json`	Контейнер подписанной записи в формате DSSE
`vouch-input-bundle.json`	Транспортный пакет с конвертом и байтами исходника и входа

Пакет имеет лимит байтов. Далее проверьте его подпись по политике получателя.

3. Аутентифицируйте пакет

lispex vouch verify \
  --bundle issued/vouch-input-bundle.json \
  --trust-policy policy.json \
  --profile csk.checked-profile/v1 \
  --report-out authenticated.json

Команда завершается с кодом 0 без вывода. В authenticated.json поле authentication_status равно "authenticated", а primary_error равно null. Это подтверждает, что допустимый ключ подписал контекст, принятый вашей политикой.

Поле отчёта comparison_status: "agree" описывает подписанную запись выполнения. Текущий запуск проверяется на шаге 5. Сначала привяжите собственные исходник и вход.

4. Привяжите свой запрос

Передайте выбранные исходник и вход отдельно от пакета.

lispex vouch verify \
  --bundle issued/vouch-input-bundle.json \
  --trust-policy policy.json \
  --source print-handoff.lspx \
  --input input.checked.json \
  --profile csk.checked-profile/v1 \
  --report-out bound.json

Команда завершается с кодом 0 без вывода. После совпадения точных байтов обоих файлов с подписанным контекстом она записывает authentication_status: "authenticated" в bound.json. Формат отчёта тот же, что на шаге 3. Привязку запроса устанавливают отдельно переданные этой команде исходник и вход.

Полностью проверенное изображение Лиспекса можно передать через --source-image вместо --source. Продолжайте явно указывать --input. Повторное выполнение и проверка допуска в Native требуют пути к исходнику и входу. Неполная пара отклоняется до чтения файлов.

5. Проверьте текущее выполнение

lispex vouch verify \
  --bundle issued/vouch-input-bundle.json \
  --trust-policy policy.json \
  --source print-handoff.lspx \
  --input input.checked.json \
  --profile csk.checked-profile/v1 \
  --reexecute \
  --report-out current.json

Команда завершается с кодом 0 без вывода. Она записывает следующие результаты в current.json.

Поле	Значение
`authentication.status`	`"authenticated"`
`reexecution.status`	`"execution-agreed"`
`comparison.current_vs_signed`	`"agree"`

Теперь Native сравнил полные текущие записи tree и Meaning с подписанными. Далее потребуйте решение, нужное приложению.

6. Потребуйте нужное решение

lispex vouch gate \
  --bundle issued/vouch-input-bundle.json \
  --trust-policy policy.json \
  --source print-handoff.lspx \
  --input input.checked.json \
  --profile csk.checked-profile/v1 \
  --require-decision approve \
  --report-out gate.json

Команда завершается с кодом 0 без вывода и создаёт gate.json. Ниже показан его объект gate.

JSON

{
  "basis": "csk.current-native-agreement/v0",
  "observed_decision": "approve",
  "reason": null,
  "required_decision": "approve",
  "status": "granted"
}

В рамках этого вызова команда аутентифицирует данные, привязывает запрос, выполняет правило заново и сравнивает требуемое решение. Локальный допуск возникает внутри процесса Native. Отчёт сохраняет результат для просмотра и журналирования.

Чтобы увидеть отказ, повторите команду с --require-decision deny и --report-out denied.json. Она завершится с кодом 10 без вывода. В отчёте появятся gate.status: "denied" и gate.reason: "required-decision-mismatch". Наблюдаемое решение останется "approve". После отказа прочитайте отчёт, прежде чем выбирать следующее действие приложения.

Вызывающее приложение проверяет личность пользователя, актуальность, срок действия и отзыв. Оно также контролирует повторное использование запросов, деловые разрешения и состояние транзакций. Внешними действиями, например разрешением печати, управляет приложение.

Добавьте компиляцию или подключите приложение

Пример компиляции добавляет согласие ВМ Лиспекса к проверкам tree и Meaning. После аутентификации запроса Native заново строит Core IR и байткод. Core IR представляет собой промежуточное представление с разрешёнными ссылками имён.

Для подключения результата локальной проверки к приложению откройте «Передача приложению». Назначение выходных файлов описано в разделе «Записи и отчёты».