Common Expression Language (CEL) to uniwersalny język wyrażeń zaprojektowany tak, aby był szybki, przenośny i bezpieczny. Możesz używać CEL samodzielnie lub osadzić go w większym produkcie. CEL doskonale sprawdza się w wielu zastosowaniach, od kierowania zdalnych wywołań procedur (RPC) po definiowanie zasad bezpieczeństwa. CEL jest rozszerzalny, niezależny od platformy, formalnie weryfikowalny i zoptymalizowany pod kątem przepływów pracy typu „skompiluj raz, oceń wiele razy”.
CEL został zaprojektowany specjalnie tak, aby bezpiecznie wykonywać kod użytkownika. Chociaż bezkrytyczne wywoływanie funkcji eval() w kodzie Pythona użytkownika jest niebezpieczne, możesz bezpiecznie wykonywać kod CEL użytkownika. CEL zapobiega też zachowaniom, które mogłyby obniżyć jego wydajność, dlatego ocenia bezpiecznie w nanosekundach lub mikrosekundach. Szybkość i bezpieczeństwo CEL sprawiają, że jest on idealny do aplikacji o krytycznym znaczeniu dla wydajności.
CEL ocenia wyrażenia podobne do funkcji jednowierszowych lub wyrażeń lambda. CEL jest zwykle używany do podejmowania decyzji logicznych, ale możesz go też używać do tworzenia bardziej złożonych obiektów, takich jak komunikaty JSON lub Protocol Buffer.
Dlaczego CEL?
Wiele usług i aplikacji ocenia konfiguracje deklaratywne. Na przykład kontrola dostępu oparta na rolach (RBAC) to konfiguracja deklaratywna, która na podstawie roli użytkownika i zbioru użytkowników podejmuje decyzję o dostępie. Konfiguracje deklaratywne wystarczają w większości przypadków, ale czasami potrzebujesz większej ekspresyjności. Wtedy przydaje się CEL.
Jako przykład rozszerzenia konfiguracji deklaratywnej za pomocą CEL rozważ możliwości usługi Google Cloud Identity and Access Management (IAM). RBAC jest typowym przypadkiem, ale IAM oferuje wyrażenia CEL, które pozwalają użytkownikom dodatkowo ograniczyć zakres uprawnień opartych na rolach zgodnie z właściwościami komunikatu proto żądania lub zasobów, do których uzyskiwany jest dostęp. Opisywanie takich warunków za pomocą modelu danych spowodowałoby powstanie skomplikowanego interfejsu API, który byłby trudny w użyciu. Zamiast tego używanie CEL z kontrolą dostępu opartą na atrybutach (ABAC) jest ekspresyjnym i zaawansowanym rozszerzeniem RBAC.
Podstawowe pojęcia CEL
W CEL wyrażenie jest kompilowane w środowisku. Krok kompilacji tworzy abstrakcyjne drzewo składni (AST) w formacie bufor protokołu. Skompilowane wyrażenia są przechowywane do wykorzystania w przyszłości, aby ocena była jak najszybsza. Pojedyncze skompilowane wyrażenie można ocenić za pomocą wielu różnych danych wejściowych.
Przyjrzyjmy się bliżej niektórym z tych pojęć.
Wyrażenia
Wyrażenia są pisane przez użytkowników. Wyrażenia są podobne do treści funkcji jednowierszowych lub wyrażeń lambda. Sygnatura funkcji, która deklaruje dane wejściowe, jest zapisywana poza wyrażeniem CEL, a biblioteka funkcji dostępnych w CEL jest importowana automatycznie.
Na przykład to wyrażenie CEL pobiera obiekt żądania, a żądanie zawiera token claims. Wyrażenie zwraca wartość logiczną wskazującą, czy token claims jest nadal ważny.
Przykładowe wyrażenie CEL do uwierzytelniania tokena claims
// 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
Użytkownicy definiują wyrażenie CEL, a usługi i aplikacje definiują środowisko, w którym jest ono uruchamiane.
Środowiska
Środowiska są definiowane przez usługi. Usługi i aplikacje, które osadzają CEL, deklarują środowisko wyrażeń. Środowisko to zbiór zmiennych i funkcji, których można używać w wyrażeniach CEL.
Na przykład ten kod textproto deklaruje środowisko zawierające zmienne request i now za pomocą komunikatu CompileRequest z usługi CEL.
Przykładowa deklaracja środowiska 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" }
}
}
Deklaracje oparte na proto są używane przez narzędzie do sprawdzania typów CEL, aby upewnić się, że wszystkie odwołania do identyfikatorów i funkcji w wyrażeniu są zadeklarowane i używane prawidłowo.
Etapy przetwarzania wyrażeń
Wyrażenia CEL są przetwarzane w 3 etapach:
- Analizuj
- Czek
- Oceń
Najczęstszym sposobem użycia CEL jest analizowanie i sprawdzanie wyrażeń w czasie konfiguracji, przechowywanie AST, a następnie pobieranie i ocenianie AST wielokrotnie w czasie działania.
Ilustracja etapów przetwarzania CEL
CEL jest analizowany z wyrażenia czytelnego dla człowieka do AST za pomocą
ANTLR. Etap analizy emituje AST oparte na proto,
w którym każdy węzeł Expr w AST zawiera identyfikator całkowity używany do
indeksowania metadanych generowanych podczas analizowania i sprawdzania. Plik
syntax.proto utworzony podczas analizowania reprezentuje
abstrakcyjną reprezentację tego, co zostało wpisane w postaci ciągu znaków
wyrażenia.
Po przeanalizowaniu wyrażenia jest ono sprawdzane pod kątem typów w środowisku, aby upewnić się, że wszystkie identyfikatory zmiennych i funkcji w wyrażeniu zostały zadeklarowane i są używane prawidłowo. Narzędzie do sprawdzania typów tworzy plik
checked.proto, który zawiera metadane dotyczące typów, zmiennych i funkcji
co może znacznie zwiększyć wydajność oceny.
Na koniec, po przeanalizowaniu i sprawdzeniu wyrażenia, przechowywane AST jest oceniane.
Oceniający CEL potrzebuje 3 rzeczy:
- Wiązania funkcji dla wszystkich rozszerzeń niestandardowych
- Wiązania zmiennych
- AST do oceny
Wiązania funkcji i zmiennych powinny być zgodne z tymi, które zostały użyte do skompilowania AST. Każde z tych danych wejściowych można ponownie wykorzystać w wielu ocenach, np. AST oceniane w wielu zestawach wiązań zmiennych, te same zmienne używane w wielu AST lub wiązania funkcji używane przez cały czas działania procesu (częsty przypadek).
Formalna weryfikacja
Oprócz oceny w czasie działania wyrażenia i zasady CEL można formalnie zweryfikować, aby matematycznie udowodnić ich poprawność w przypadku wszystkich możliwych danych wejściowych.
Dzięki narzędziu do sprawdzania twierdzeń Z3 platforma CEL Formal Verification Framework w CEL-Java tłumaczy wyrażenia i zasady CEL na formuły Satisfiability Modulo Theories (SMT), aby:
- Udowodnić niezmienniki bezpieczeństwa: sprawdź, czy nie można obejść krytycznych zasad przy żadnej kombinacji danych wejściowych, używając specyfikacji
assumeiassert. - Sprawdzić równoważność logiczną: matematycznie udowodnij, że refaktoryzowane lub wygenerowane przez AI wyrażenia zachowują się identycznie jak pierwotna reguła.
- Wymusić wyczerpującą ważność: zagwarantuj, że zabezpieczenia (np. zasady weryfikacji przyjmowania w Kubernetes) obowiązują w przypadku wszystkich danych wejściowych, lub wygeneruj konkretne kontrprzykłady w przypadku naruszenia.
- Eliminować fałszywe alarmy: użyj 3-etapowego śledzenia zanieczyszczeń, aby odizolować niestandardowe funkcje, które nie są mapowane, dzięki czemu zgłaszane naruszenia są zawsze powtarzalnymi błędami.
Więcej informacji i przykłady z życia wzięte znajdziesz w poście na blogu Google Open Source: Securing the agentic era: Introducing formal verification for CEL.