Langage CEL (Common Expression Language)

Le CEL (Common Expression Language) est un langage d'expression à usage général conçu pour être rapide, portable et sûr à exécuter. Vous pouvez utiliser le CEL seul ou l'intégrer dans un produit plus volumineux. Le CEL est idéal pour une grande variété d'applications, du routage des appels de procédure à distance (RPC) à la définition des règles de sécurité. Le CEL est extensible, indépendant de la plate-forme, formellement vérifiable et optimisé pour les workflows de compilation unique/évaluation multiple.

Le CEL a été conçu spécifiquement pour être sûr lors de l'exécution du code utilisateur. Bien qu'il soit dangereux d'appeler aveuglément eval() sur le code Python d'un utilisateur, vous pouvez exécuter en toute sécurité le code CEL d'un utilisateur. De plus, comme le CEL empêche les comportements qui le rendraient moins performant, il s'évalue en toute sécurité en quelques nanosecondes ou microsecondes. La rapidité et la sécurité du CEL le rendent idéal pour les applications critiques en termes de performances.

Le CEL évalue les expressions semblables à des fonctions sur une seule ligne ou à des expressions lambda. Bien que le CEL soit couramment utilisé pour les décisions booléennes, vous pouvez également l'utiliser pour créer des objets plus complexes tels que des messages JSON ou des messages de tampon de protocole.

Pourquoi utiliser le CEL ?

De nombreux services et applications évaluent les configurations déclaratives. Par exemple, le contrôle des accès basé sur les rôles (RBAC) est une configuration déclarative qui produit une décision d'accès en fonction d'un rôle utilisateur et d'un ensemble d'utilisateurs. Bien que les configurations déclaratives soient suffisantes dans la plupart des cas, vous avez parfois besoin de plus de puissance expressive. C'est là qu'intervient le CEL.

Pour illustrer l'extension d'une configuration déclarative avec le CEL, examinons les fonctionnalités de Google Cloud Identity and Access Management (IAM). Bien que le RBAC soit le cas courant, IAM propose des expressions CEL pour permettre aux utilisateurs de limiter davantage le champ d'application de l'octroi basé sur les rôles en fonction des propriétés du message proto de la requête ou des ressources auxquelles ils accèdent. La description de ces conditions via le modèle de données entraînerait une surface d'API complexe et difficile à utiliser. Au lieu de cela, l'utilisation du CEL avec le contrôle des accès basé sur les attributs (ABAC) est une extension expressive et puissante du RBAC.

Concepts de base du CEL

Dans le CEL, une expression est compilée par rapport à un environnement. L'étape de compilation produit un arbre de syntaxe abstrait (AST) au format de tampon de protocole. Les expressions compilées sont stockées pour une utilisation ultérieure afin de rendre l'évaluation aussi rapide que possible. Une seule expression compilée peut être évaluée avec de nombreuses entrées différentes.

Examinons de plus près certains de ces concepts.

Expressions

Les expressions sont écrites par les utilisateurs. Les expressions sont semblables à des corps de fonction sur une seule ligne ou à des expressions lambda. La signature de fonction qui déclare l'entrée est écrite en dehors de l'expression CEL, et la bibliothèque de fonctions disponible pour le CEL est importée automatiquement.

Par exemple, l'expression CEL suivante prend un objet de requête, et la requête inclut un jeton claims. L'expression renvoie une valeur booléenne indiquant si le jeton claims est toujours valide.

Exemple d'expression CEL pour authentifier un jeton de revendications

// 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

Alors que les utilisateurs définissent l'expression CEL, les services et les applications définissent l'environnement dans lequel elle s'exécute.

Environnements

Les environnements sont définis par les services. Les services et les applications qui intègrent le CEL déclarent l'environnement d'expression. L'environnement est l'ensemble des variables et des fonctions qui peuvent être utilisées dans les expressions CEL.

Par exemple, le code textproto suivant déclare un environnement contenant les variables request et now à l'aide du message CompileRequest d'un service CEL.

Exemple de déclaration d'environnement 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" }
  }
}

Les déclarations basées sur proto sont utilisées par le vérificateur de type CEL pour s'assurer que toutes les références d'identifiant et de fonction d'une expression sont déclarées et utilisées correctement.

Phases de traitement des expressions

Les expressions CEL sont traitées en trois phases :

  1. Analyser
  2. Vérifier
  3. Évaluer

Le modèle d'utilisation le plus courant du CEL consiste à analyser et à vérifier les expressions au moment de la configuration, à stocker l'AST, puis à récupérer et à évaluer l'AST de manière répétée au moment de l'exécution.

Illustration des phases de traitement du CEL

Les expressions sont analysées et vérifiées sur les chemins de configuration, stockées, puis évaluées par rapport à un ou plusieurs contextes sur les chemins de lecture.

Le CEL est analysé à partir d'une expression lisible par l'homme vers un AST à l'aide d'une ANTLR. La phase d'analyse émet un AST basé sur proto où chaque Expr nœud de l'AST contient un ID entier utilisé pour indexer les métadonnées générées lors de l'analyse et de la vérification. Le syntax.proto fichier produit lors de l'analyse représente la représentation abstraite de ce qui a été saisi dans la forme de chaîne de l' expression.

Une fois qu'une expression est analysée, son type est vérifié par rapport à l'environnement pour s'assurer que tous les identifiants de variable et de fonction de l'expression ont été déclarés et sont utilisés correctement. Le vérificateur de type produit un checked.proto fichier qui inclut des métadonnées de résolution de type, de variable et de fonction qui peuvent améliorer considérablement l'efficacité de l'évaluation.

Enfin, une fois qu'une expression est analysée et vérifiée, l'AST stocké est évalué.

L'évaluateur CEL a besoin de trois éléments :

  • Des liaisons de fonction pour toutes les extensions personnalisées
  • Des liaisons de variables
  • Un AST à évaluer

Les liaisons de fonction et de variable doivent correspondre à ce qui a été utilisé pour compiler l'AST. Ces entrées peuvent être réutilisées dans plusieurs évaluations, par exemple un AST évalué sur plusieurs ensembles de liaisons de variables, les mêmes variables utilisées par rapport à plusieurs AST ou les liaisons de fonction utilisées pendant la durée de vie d'un processus (cas courant).

Vérification formelle

En plus de l'évaluation au moment de l'exécution, les expressions et les règles CEL peuvent être formellement vérifiées pour prouver mathématiquement leur exactitude sur toutes les entrées possibles.

Basé sur le prouveur de théorèmes Z3, le framework de vérification formelle CEL dans CEL-Java traduit les expressions et les règles CEL en formules de satisfiabilité modulo théories (SMT) pour :

  • Prouver les invariants de sécurité : vérifiez que les règles critiques ne peuvent pas être contournées sous aucune combinaison d'entrées à l'aide des spécifications assume et assert.
  • Vérifier l'équivalence logique : prouvez mathématiquement que les expressions refactorisées ou générées par l'IA se comportent de manière identique à la règle d'origine.
  • Appliquer une validité exhaustive : garantissez que les garde-fous (tels que les règles d'admission de validation Kubernetes) s'appliquent à toutes les entrées ou générez des contre-exemples concrets en cas de violation.
  • Éliminer les faux positifs : utilisez le suivi de la contamination en trois passes pour isoler les fonctions personnalisées non mappées, en vous assurant que les violations signalées sont toujours des bugs reproductibles.

Pour une introduction et des exemples concrets, consultez l'article de blog Google Open Source : Securing the agentic era: Introducing formal verification for CEL (Sécuriser l'ère agentique : présentation de la vérification formelle pour le CEL).