Общий язык выражений (CEL)

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

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

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

Почему именно 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 на основе прототипов, где каждый узел Expr содержит целочисленный идентификатор, используемый для индексации метаданных, сгенерированных во время анализа и проверки. Создаваемый во время анализа файл syntax.proto представляет собой абстрактное представление того, что было введено в строковой форме выражения.

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

Наконец, после того как выражение будет проанализировано и проверено, сохраненное абстрактное синтаксическое дерево (AST) будет вычислено.

Для проведения оценки CEL необходимы три вещи:

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

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

Формальная проверка

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

Благодаря механизму доказательства теорем Z3 , платформа формальной верификации CEL в CEL-Java преобразует выражения и политики CEL в формулы выполнимости по модулю теорий (SMT):

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

Для ознакомления и примеров из реальной жизни см. сообщение в блоге Google Open Source: Обеспечение безопасности в эпоху агентного управления: внедрение формальной верификации для CEL .

Связанные ресурсы

• Учебное пособие по CEL
• Определение языка
• Руководство по функциональным функциям
• Официальное объявление о подтверждении
• Репозиторий CEL Java Verifier

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

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

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

Почему именно 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 на основе прототипов, где каждый узел Expr содержит целочисленный идентификатор, используемый для индексации метаданных, сгенерированных во время анализа и проверки. Создаваемый во время анализа файл syntax.proto представляет собой абстрактное представление того, что было введено в строковой форме выражения.

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

Наконец, после того как выражение будет проанализировано и проверено, сохраненное абстрактное синтаксическое дерево (AST) будет вычислено.

Для проведения оценки CEL необходимы три вещи:

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

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

Формальная проверка

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

Благодаря механизму доказательства теорем Z3 , платформа формальной верификации CEL в CEL-Java преобразует выражения и политики CEL в формулы выполнимости по модулю теорий (SMT):

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

Для ознакомления и примеров из реальной жизни см. сообщение в блоге Google Open Source: Обеспечение безопасности в эпоху агентного управления: внедрение формальной верификации для CEL .

Связанные ресурсы

• Учебное пособие по CEL
• Определение языка
• Руководство по функциональным функциям
• Официальное объявление о подтверждении
• Репозиторий CEL Java Verifier

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

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

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

Почему именно 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 на основе прототипов, где каждый узел Expr содержит целочисленный идентификатор, используемый для индексации метаданных, сгенерированных во время анализа и проверки. Создаваемый во время анализа файл syntax.proto представляет собой абстрактное представление того, что было введено в строковой форме выражения.

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

Наконец, после того как выражение будет проанализировано и проверено, сохраненное абстрактное синтаксическое дерево (AST) будет вычислено.

Для проведения оценки CEL необходимы три вещи:

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

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

Формальная проверка

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

Благодаря механизму доказательства теорем Z3 , платформа формальной верификации CEL в CEL-Java преобразует выражения и политики CEL в формулы выполнимости по модулю теорий (SMT):

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

Для ознакомления и примеров из реальной жизни см. сообщение в блоге Google Open Source: Обеспечение безопасности в эпоху агентного управления: внедрение формальной верификации для CEL .

Связанные ресурсы

• Учебное пособие по CEL
• Определение языка
• Руководство по функциональным функциям
• Официальное объявление о подтверждении
• Репозиторий CEL Java Verifier

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

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

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

Почему именно 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 на основе прототипов, где каждый узел Expr содержит целочисленный идентификатор, используемый для индексации метаданных, сгенерированных во время анализа и проверки. Создаваемый во время анализа файл syntax.proto представляет собой абстрактное представление того, что было введено в строковой форме выражения.

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

Наконец, после того как выражение будет проанализировано и проверено, сохраненное абстрактное синтаксическое дерево (AST) будет вычислено.

Для проведения оценки CEL необходимы три вещи:

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

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

Формальная проверка

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

Благодаря механизму доказательства теорем Z3 , платформа формальной верификации CEL в CEL-Java преобразует выражения и политики CEL в формулы выполнимости по модулю теорий (SMT):

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

Для ознакомления и примеров из реальной жизни см. сообщение в блоге Google Open Source: Обеспечение безопасности в эпоху агентного управления: внедрение формальной верификации для CEL .

Связанные ресурсы

• Учебное пособие по CEL
• Определение языка
• Руководство по функциональным функциям
• Официальное объявление о подтверждении
• Репозиторий CEL Java Verifier