{i>Common Expression Language

Common Expression Language (CEL) adalah bahasa ekspresi tujuan umum yang dirancang agar cepat, portabel, dan aman untuk dieksekusi. Anda dapat menggunakan CEL secara terpisah atau menyematkannya ke dalam produk yang lebih besar. CEL sangat cocok untuk berbagai aplikasi, mulai dari merutekan panggilan prosedur jarak jauh (RPC) hingga menentukan kebijakan keamanan. CEL dapat diperluas, tidak bergantung pada platform, dapat diverifikasi secara formal, dan dioptimalkan untuk alur kerja kompilasi sekali/evaluasi berkali-kali.

CEL dirancang khusus agar aman untuk mengeksekusi kode pengguna. Meskipun berbahaya untuk memanggil eval() secara membabi buta pada kode python pengguna, Anda dapat menjalankan kode CEL pengguna dengan aman. Selain itu, karena CEL mencegah perilaku yang akan membuatnya kurang berperforma, CEL dievaluasi dengan aman dalam nanodetik atau mikrodetik. Kecepatan dan keamanan CEL menjadikannya ideal untuk aplikasi yang penting performanya.

CEL mengevaluasi ekspresi yang mirip dengan fungsi satu baris atau ekspresi lambda. Meskipun umumnya digunakan untuk keputusan boolean, CEL juga dapat digunakan untuk membuat objek yang lebih kompleks seperti pesan JSON atau buffer protokol.

Mengapa CEL?

Banyak layanan dan aplikasi mengevaluasi konfigurasi deklaratif. Misalnya, role-based access control (RBAC) adalah konfigurasi deklaratif yang menghasilkan keputusan akses berdasarkan peran pengguna dan sekumpulan pengguna. Meskipun konfigurasi deklaratif sudah cukup untuk sebagian besar kasus, terkadang Anda memerlukan kemampuan ekspresif yang lebih besar. Di sinilah CEL berperan.

Sebagai contoh memperluas konfigurasi deklaratif dengan CEL, pertimbangkan kemampuan Identity and Access Management (IAM) Google Cloud. Meskipun RBAC adalah kasus umum, IAM menawarkan ekspresi CEL untuk memungkinkan pengguna membatasi lebih lanjut cakupan pemberian berbasis peran sesuai dengan properti pesan proto permintaan atau resource yang diakses. Mendeskripsikan kondisi tersebut melalui model data akan menghasilkan permukaan API yang rumit dan sulit digunakan. Sebagai gantinya, penggunaan CEL dengan kontrol akses berbasis atribut (ABAC) adalah ekstensi RBAC yang ekspresif dan canggih.

Konsep inti CEL

Di CEL, ekspresi dikompilasi terhadap lingkungan. Langkah kompilasi menghasilkan abstract syntax tree (AST) dalam format protocol buffer. Ekspresi yang dikompilasi disimpan untuk digunakan pada masa mendatang agar evaluasi tetap secepat mungkin. Satu ekspresi yang dikompilasi dapat dievaluasi dengan banyak input yang berbeda.

Berikut adalah pembahasan lebih mendalam tentang beberapa konsep ini.

Ekspresi

Ekspresi ditulis oleh pengguna. Ekspresi mirip dengan isi fungsi satu baris atau ekspresi lambda. Tanda tangan fungsi yang mendeklarasikan input ditulis di luar ekspresi CEL, dan library fungsi yang tersedia untuk CEL diimpor secara otomatis.

Misalnya, ekspresi CEL berikut mengambil objek permintaan, dan permintaan menyertakan token claims. Ekspresi menampilkan nilai boolean yang menunjukkan apakah token claims masih valid.

Contoh ekspresi CEL untuk mengautentikasi token klaim

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

Saat pengguna menentukan ekspresi CEL, layanan dan aplikasi menentukan lingkungan tempat ekspresi tersebut berjalan.

Lingkungan

Lingkungan ditentukan oleh layanan. Layanan dan aplikasi yang menyematkan CEL mendeklarasikan lingkungan ekspresi. Lingkungan adalah kumpulan variabel dan fungsi yang dapat digunakan dalam ekspresi CEL.

Misalnya, kode textproto berikut mendeklarasikan lingkungan yang berisi variabel request dan now menggunakan pesan CompileRequest dari layanan CEL.

Contoh deklarasi lingkungan 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" }
  }
}

Deklarasi berbasis proto digunakan oleh pemeriksa jenis CEL untuk memastikan bahwa semua referensi fungsi dan ID dalam ekspresi dideklarasikan dan digunakan dengan benar.

Fase pemrosesan ekspresi

Ekspresi CEL diproses dalam tiga fase:

  1. Parse
  2. Cek
  3. Evaluasi

Pola penggunaan CEL yang paling umum adalah mengurai dan memeriksa ekspresi pada waktu konfigurasi, menyimpan AST, lalu mengambil dan mengevaluasi AST berulang kali pada waktu runtime.

Ilustrasi fase pemrosesan CEL

Ekspresi diuraikan dan diperiksa di jalur konfigurasi, disimpan, lalu dievaluasi terhadap satu atau beberapa konteks di jalur baca.

CEL diuraikan dari ekspresi yang mudah dibaca manusia ke AST menggunakan tata bahasa parser dan leksikal ANTLR. Fase penguraian memancarkan AST berbasis proto di mana setiap node Expr dalam AST berisi ID bilangan bulat yang digunakan untuk mengindeks metadata yang dihasilkan selama penguraian dan pemeriksaan. File syntax.proto yang dihasilkan selama penguraian merepresentasikan representasi abstrak dari apa yang diketik dalam bentuk string ekspresi.

Setelah ekspresi diuraikan, ekspresi tersebut kemudian diperiksa jenisnya terhadap lingkungan untuk memastikan semua ID variabel dan fungsi dalam ekspresi telah dideklarasikan dan digunakan dengan benar. Pemeriksa jenis menghasilkan file checked.proto yang mencakup metadata resolusi jenis, variabel, dan fungsi yang dapat meningkatkan efisiensi evaluasi secara drastis.

Terakhir, setelah ekspresi diuraikan dan diperiksa, AST yang disimpan akan dievaluasi.

Evaluator CEL memerlukan tiga hal:

  • Pengikatan fungsi untuk ekstensi kustom
  • Binding variabel
  • AST yang akan dievaluasi

Binding fungsi dan variabel harus cocok dengan yang digunakan untuk mengompilasi AST. Input ini dapat digunakan kembali di beberapa evaluasi, seperti AST yang dievaluasi di banyak set pengikatan variabel, variabel yang sama yang digunakan terhadap banyak AST, atau pengikatan fungsi yang digunakan selama masa aktif proses (kasus umum).

Verifikasi formal

Selain evaluasi runtime, ekspresi dan kebijakan CEL dapat diverifikasi secara formal untuk membuktikan kebenarannya secara matematis di semua kemungkinan input.

Didukung oleh pembuktian teorema Z3, Framework Verifikasi Formal CEL di CEL-Java menerjemahkan ekspresi dan Kebijakan CEL ke dalam formula Satisfiability Modulo Theories (SMT) untuk:

  • Membuktikan invarian keamanan: Verifikasi bahwa kebijakan penting tidak dapat dilewati dalam kombinasi input apa pun menggunakan spesifikasi assume dan assert.
  • Verifikasi kesetaraan logis: Buktikan secara matematis bahwa ekspresi yang di-refactor atau dibuat AI berperilaku sama dengan aturan aslinya.
  • Terapkan validitas menyeluruh: Pastikan bahwa pembatasan (seperti Kebijakan Penerimaan Validasi Kubernetes) berlaku di semua input, atau buat contoh sanggahan konkret jika dilanggar.
  • Menghilangkan positif palsu: Gunakan pelacakan pencemaran tiga tahap untuk mengisolasi fungsi kustom yang tidak dipetakan, sehingga memastikan bahwa pelanggaran yang dilaporkan selalu berupa bug yang dapat direproduksi.

Untuk pengantar dan contoh dunia nyata, lihat postingan blog Google Open Source: Securing the agentic era: Introducing formal verification for CEL.