OpenShell описал, как с помощью Z3, решателя логических ограничений, формально проверять изменения прав, которые предлагают ИИ-агенты. Проверка выясняет, может ли предложенная политика разрешить действие, которое не разрешает эталонная политика.
Для сетевого действия проверяющий модуль OpenShell моделирует исполняемый файл, хост, порт, сетевой уровень, HTTP-метод и путь.
Перед утверждением каждой предложенной политики OpenShell запускает четыре встроенные экспертные проверки безопасности.
Проверка утверждений:
- OpenShell описал применение Z3 для формальной проверки того, остаётся ли предложенное ИИ-агентом изменение политики в пределах уже утверждённых прав. (подтверждено самой публикацией: доказательство; «In this post- we’ll dive into how permission review breaks at agent scale, and how to use the Z3 open source library to write a formal proof that a policy change proposed by an agent stays inside what you approved.»)
- Проверка выясняет, может ли предложенная политика разрешить действие, которое не разрешает эталонная политика. (подтверждено самой публикацией: доказательство; «asks if a proposed policy can do any actions that a expert pre-defined policy (for example, Github read-only) cannot do.»)
- Для сетевого действия проверяющий модуль OpenShell моделирует исполняемый файл, хост, порт, сетевой уровень, HTTP-метод и путь. (подтверждено самой публикацией: доказательство; «OpenShell’s runtime prover models the following attributes for any network action: action = { binary: String, host: String, port: Int, layer: String, method: String, path: String }»)
- Перед утверждением каждой предложенной политики OpenShell запускает четыре встроенные экспертные проверки безопасности. (подтверждено самой публикацией: доказательство; «Today, the OpenShell policy prover encodes the following expert queries which run on every proposed policy before approval.»)
Первоисточники:
оценка 65,3 из 100 · тип: руководство