Common Expression Language (CEL)

Common Expression Language (CEL) – это язык выражений общего назначения, разработанный для быстрого, переносимого и безопасного выполнения. Вы можете использовать CEL отдельно или встроить его в более крупный продукт. CEL отлично подходит для самых разных приложений – от маршрутизации вызовов удаленных процедур (RPC) до определения правил безопасности. CEL – это расширяемый, независимый от платформы и формально проверяемый язык, оптимизированный для рабочих процессов, в которых компиляция выполняется один раз, а оценка – многократно.

Язык CEL был разработан специально для безопасного выполнения пользовательского кода. В то время как слепо вызывать eval() для пользовательского кода Python опасно, вы можете безопасно выполнять пользовательский код CEL. А поскольку CEL предотвращает поведение, которое может снизить производительность, оценка выполняется безопасно за нано- или микросекунды. Скорость и безопасность CEL делают его идеальным для приложений, критичных к производительности.

CEL оценивает выражения, похожие на однострочные функции или лямбда-выражения. Хотя CEL обычно используется для логических решений, вы также можете использовать его для создания более сложных объектов, таких как JSON или сообщения буфера протокола.

Почему CEL?

Многие сервисы и приложения оценивают декларативные конфигурации. Например, контроль доступа на основе ролей (RBAC) – это декларативная конфигурация, которая принимает решение о доступе на основе роли пользователя и набора пользователей. Хотя декларативных конфигураций достаточно для большинства случаев, иногда вам нужно больше выразительной силы. Вот тут-то и пригодится CEL.

В качестве примера расширения декларативной конфигурации с помощью CEL рассмотрим возможности Google Cloud Identity and Access Management (IAM). Хотя RBAC является распространенным случаем, IAM предлагает выражения CEL, позволяющие пользователям дополнительно ограничивать область предоставления на основе ролей в соответствии со свойствами протосообщения запроса или ресурсов, к которым осуществляется доступ. Если бы мы попытались описать такие условия в модели данных, то получили бы сложный API, с которым было бы трудно работать. Вместо этого использование CEL с управлением доступом на основе атрибутов (ABAC) является выразительным и мощным расширением RBAC.

Основные понятия CEL

В CEL выражение компилируется в соответствии со средой. На этапе компиляции создается абстрактное синтаксическое дерево (AST) в формате буфера протокола. Скомпилированные выражения сохраняются для дальнейшего использования, чтобы вычисления выполнялись как можно быстрее. Одно скомпилированное выражение можно вычислить с разными входными данными.

Ниже мы подробнее рассмотрим некоторые из этих понятий.

Выражения

Выражения пишутся пользователями. Выражения похожи на однострочные тела функций или лямбда-выражения. Сигнатура функции, объявляющая входные данные, записывается за пределами выражения CEL, а библиотека функций, доступных для CEL, импортируется автоматически.

Например, следующее выражение CEL принимает объект запроса, который включает токен claims. Выражение возвращает логическое значение, которое указывает, действителен ли токен claims.

Пример выражения CEL для аутентификации токена утверждений

// Check whether a JSON Web Token has expired by inspecting the 'exp' claim.
//
// Args:
//   claims - authentication claims.
//   now    - timestamp indicating the current system time.
// Returns: true if the token has expired.
//
timestamp(claims["exp"]) < now

Пользователи определяют выражение CEL, а сервисы и приложения – среду, в которой оно выполняется.

Среды

Среды определяются сервисами. Сервисы и приложения, в которые встроен CEL, объявляют среду выражения. Среда – это набор переменных и функций, которые можно использовать в выражениях CEL.

Например, в следующем коде textproto объявляется среда, содержащая переменные request и now, с использованием сообщения CompileRequest из сервиса CEL.

Пример объявления среды CEL

# Format: $SOURCE_PATH/service.proto#CompileRequest
declarations {
  name: "request"
  ident {
    type { message_type: "google.rpc.context.AttributeContext.Request" }
  }
}
declarations {
  name: "now"
  ident {
    type { well_known: "TIMESTAMP" }
  }
}

Объявления на основе прототипов используются средством проверки типов CEL, чтобы убедиться, что все ссылки на идентификаторы и функции в выражении объявлены и используются правильно.

Этапы обработки выражений

Выражения CEL обрабатываются в три этапа:

  1. Синтаксический анализ
  2. Чек
  3. Оценка

Наиболее распространенный шаблон использования CEL – синтаксический анализ и проверка выражений во время настройки, сохранение AST, а затем многократное извлечение и оценка AST во время выполнения.

Иллюстрация этапов обработки CEL

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

CEL преобразуется из человекочитаемого выражения в AST с помощью лексического и синтаксического анализатора ANTLR. На этапе синтаксического анализа создается AST на основе proto, где каждый узел Expr в AST содержит целочисленный идентификатор, который используется для индексации метаданных, созданных во время синтаксического анализа и проверки. Файл syntax.proto, созданный во время синтаксического анализа, представляет собой абстрактное представление того, что было введено в строковой форме выражения.

После синтаксического анализа выражения выполняется проверка типов в среде, чтобы убедиться, что все идентификаторы переменных и функций в выражении объявлены и используются правильно. Средство проверки типов создает файл checked.proto, который содержит метаданные разрешения типов, переменных и функций. Это позволяет значительно повысить эффективность оценки.

Наконец, после того как выражение проанализировано и проверено, оценивается сохраненное AST.

Для работы оценщика CEL нужны три вещи:

  • Привязки функций для любых пользовательских расширений.
  • Привязки переменных
  • AST для оценки.

Привязки функций и переменных должны соответствовать тем, которые использовались для компиляции AST. Любые из этих входных данных можно использовать повторно в нескольких вычислениях, например AST можно вычислять для нескольких наборов привязок переменных, одни и те же переменные можно использовать для нескольких AST, а привязки функций можно использовать в течение всего времени существования процесса (распространенный случай).

Формальная верификация

Помимо оценки во время выполнения, выражения и правила CEL можно формально проверить, чтобы математически доказать их правильность для всех возможных входных данных.

Фреймворк формальной верификации CEL в CEL-Java, работающий на основе Z3 Theorem Prover, преобразует выражения и правила CEL в формулы SMT (Satisfiability Modulo Theories), чтобы:

  • Доказывать инварианты безопасности. Проверять, что критически важные правила нельзя обойти ни при каком сочетании входных данных, используя спецификации assume и assert.
  • Проверьте логическую эквивалентность. Математически докажите, что выражения, полученные в результате рефакторинга или созданные ИИ, ведут себя так же, как исходное правило.
  • Обеспечение полной валидности. Гарантируйте, что ограничения (например, правила проверки доступа Kubernetes) соблюдаются для всех входных данных, или генерируйте конкретные контрпримеры при их нарушении.
  • Устранение ложноположительных результатов. Используйте трехпроходное отслеживание уязвимостей, чтобы изолировать несопоставленные пользовательские функции и гарантировать, что зарегистрированные нарушения всегда являются воспроизводимыми ошибками.

Вводную информацию и примеры из реальной жизни можно найти в записи блога Google ПО с открытым исходным кодом Securing the agentic era: Introducing formal verification for CEL (Безопасность в эпоху агентов: представляем формальную верификацию для CEL).