Ngôn ngữ diễn đạt phổ biến (CEL)

Ngôn ngữ biểu thức thông thường (CEL) là một ngôn ngữ biểu thức đa năng được thiết kế để thực thi nhanh, di động và an toàn. Bạn có thể sử dụng CEL riêng hoặc nhúng CEL vào một sản phẩm lớn hơn. CEL phù hợp với nhiều ứng dụng, từ định tuyến các lệnh gọi thủ tục từ xa (RPC) đến xác định các chính sách bảo mật. CEL có thể mở rộng, độc lập với nền tảng, có thể xác minh chính thức và được tối ưu hoá cho quy trình công việc biên dịch một lần/đánh giá nhiều lần.

CEL được thiết kế riêng để đảm bảo an toàn khi thực thi mã người dùng. Mặc dù việc gọi eval() một cách mù quáng trên mã python của người dùng là nguy hiểm, nhưng bạn có thể thực thi mã CEL của người dùng một cách an toàn. Và vì CEL ngăn chặn hành vi làm giảm hiệu suất, nên CEL đánh giá một cách an toàn trong vài nano giây hoặc micro giây. Tốc độ và độ an toàn của CEL khiến ngôn ngữ này trở nên lý tưởng cho các ứng dụng quan trọng về hiệu suất.

CEL đánh giá các biểu thức tương tự như các hàm một dòng hoặc biểu thức lambda. Mặc dù CEL thường được dùng cho các quyết định boolean, nhưng bạn cũng có thể dùng CEL để tạo các đối tượng phức tạp hơn như JSON hoặc thông báo đệm giao thức.

Tại sao nên dùng CEL?

Nhiều dịch vụ và ứng dụng đánh giá các cấu hình khai báo. Ví dụ: kiểm soát truy cập dựa trên vai trò (RBAC) là một cấu hình khai báo tạo ra quyết định truy cập dựa trên vai trò người dùng và một nhóm người dùng. Mặc dù cấu hình khai báo là đủ cho hầu hết các trường hợp, nhưng đôi khi bạn cần có sức mạnh biểu đạt nhiều hơn. Đó là lúc CEL xuất hiện.

Ví dụ về việc mở rộng cấu hình khai báo bằng CEL, hãy xem xét các chức năng của dịch vụ Quản lý danh tính và quyền truy cập (IAM) trên Google Cloud. Mặc dù RBAC là trường hợp phổ biến, nhưng IAM cung cấp các biểu thức CEL để cho phép người dùng hạn chế thêm phạm vi cấp quyền dựa trên vai trò theo các thuộc tính thông báo proto của yêu cầu hoặc tài nguyên đang được truy cập. Việc mô tả những điều kiện như vậy thông qua mô hình dữ liệu sẽ dẫn đến một giao diện API phức tạp và khó sử dụng. Thay vào đó, việc sử dụng CEL với tính năng kiểm soát quyền truy cập dựa trên thuộc tính (ABAC) là một tiện ích mạnh mẽ và có tính biểu đạt cho RBAC.

Các khái niệm cốt lõi của CEL

Trong CEL, một biểu thức được biên dịch dựa trên một môi trường. Bước biên dịch tạo ra một cây cú pháp trừu tượng (AST) ở định dạng vùng đệm giao thức. Các biểu thức đã biên dịch được lưu trữ để sử dụng sau này nhằm duy trì tốc độ đánh giá nhanh nhất có thể. Bạn có thể đánh giá một biểu thức đã biên dịch duy nhất bằng nhiều đầu vào khác nhau.

Sau đây là thông tin chi tiết hơn về một số khái niệm này.

Cụm từ

Người dùng viết biểu thức. Biểu thức tương tự như phần nội dung hàm một dòng hoặc biểu thức lambda. Chữ ký hàm khai báo dữ liệu đầu vào được viết bên ngoài biểu thức CEL và thư viện hàm có sẵn cho CEL sẽ được tự động nhập.

Ví dụ: biểu thức CEL sau đây lấy một đối tượng yêu cầu và yêu cầu này bao gồm một mã thông báo claims. Biểu thức này trả về một giá trị boolean cho biết mã thông báo claims vẫn còn hiệu lực hay không.

Ví dụ về biểu thức CEL để xác thực mã thông báo xác nhận quyền sở hữu

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

Trong khi người dùng xác định biểu thức CEL, các dịch vụ và ứng dụng sẽ xác định môi trường nơi biểu thức đó chạy.

Môi trường

Môi trường được xác định bằng các dịch vụ. Các dịch vụ và ứng dụng nhúng CEL khai báo môi trường biểu thức. Môi trường là tập hợp các biến và hàm có thể dùng trong biểu thức CEL.

Ví dụ: mã textproto sau đây khai báo một môi trường chứa các biến requestnow bằng cách sử dụng thông báo CompileRequest từ một dịch vụ CEL.

Ví dụ về nội dung khai báo môi trường 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" }
  }
}

Trình kiểm tra loại CEL dùng các khai báo dựa trên giao thức để đảm bảo rằng tất cả các giá trị nhận dạng và hàm tham chiếu trong một biểu thức đều được khai báo và sử dụng đúng cách.

Các giai đoạn xử lý biểu thức

Các biểu thức CEL được xử lý theo 3 giai đoạn:

  1. Phân tích cú pháp
  2. Séc
  3. Đánh giá

Mẫu sử dụng CEL phổ biến nhất là phân tích cú pháp và kiểm tra các biểu thức tại thời điểm định cấu hình, lưu trữ AST, sau đó truy xuất và đánh giá AST nhiều lần tại thời điểm chạy.

Hình minh hoạ các giai đoạn xử lý CEL

Các biểu thức được phân tích cú pháp và kiểm tra trên các đường dẫn cấu hình, được lưu trữ, rồi được đánh giá dựa trên một hoặc nhiều bối cảnh trên các đường dẫn đọc.

CEL được phân tích cú pháp từ một biểu thức mà con người có thể đọc được thành một AST bằng cách sử dụng ngữ pháp trình phân tích cú pháp và trình phân tích từ vựng ANTLR. Giai đoạn phân tích cú pháp phát ra một AST dựa trên giao thức, trong đó mỗi nút Expr trong AST chứa một mã nhận dạng số nguyên được dùng để lập chỉ mục vào siêu dữ liệu được tạo trong quá trình phân tích cú pháp và kiểm tra. Tệp syntax.proto được tạo trong quá trình phân tích cú pháp biểu thị biểu thức trừu tượng của nội dung đã nhập ở dạng chuỗi của biểu thức.

Sau khi được phân tích cú pháp, biểu thức sẽ được kiểm tra kiểu dựa trên môi trường để đảm bảo tất cả các giá trị nhận dạng biến và hàm trong biểu thức đã được khai báo và đang được sử dụng đúng cách. Trình kiểm tra kiểu tạo ra một tệp checked.proto bao gồm siêu dữ liệu phân giải kiểu, biến và hàm có thể cải thiện đáng kể hiệu quả đánh giá.

Cuối cùng, sau khi một biểu thức được phân tích cú pháp và kiểm tra, AST được lưu trữ sẽ được đánh giá.

Trình đánh giá CEL cần 3 điều kiện:

  • Liên kết hàm cho mọi tiện ích tuỳ chỉnh
  • Các mối liên kết biến
  • Một AST để đánh giá

Các liên kết hàm và biến phải khớp với những gì đã dùng để biên dịch AST. Bạn có thể dùng lại bất kỳ đầu vào nào trong số này trên nhiều lượt đánh giá, chẳng hạn như AST được đánh giá trên nhiều nhóm liên kết biến, các biến giống nhau được dùng cho nhiều AST hoặc các liên kết hàm được dùng trong suốt thời gian hoạt động của một quy trình (trường hợp phổ biến).

Xác minh chính thức

Ngoài việc đánh giá thời gian chạy, các biểu thức và chính sách CEL có thể được xác minh chính thức để chứng minh tính chính xác của chúng về mặt toán học trên tất cả các đầu vào có thể.

Được hỗ trợ bởi trình chứng minh định lý Z3, Khung xác minh chính thức CEL trong CEL-Java sẽ dịch các biểu thức và Chính sách CEL thành các công thức SMT (Satisfiability Modulo Theories) để:

  • Chứng minh các bất biến bảo mật: Xác minh rằng không thể bỏ qua các chính sách quan trọng trong mọi tổ hợp đầu vào bằng cách sử dụng các quy cách assumeassert.
  • Xác minh tính tương đương logic: Chứng minh bằng toán học rằng các biểu thức được tái cấu trúc hoặc do AI tạo ra hoạt động giống hệt như quy tắc ban đầu.
  • Thực thi tính hợp lệ toàn diện: Đảm bảo rằng các biện pháp bảo vệ (chẳng hạn như Chính sách chấp nhận xác thực Kubernetes) được áp dụng cho tất cả các đầu vào hoặc tạo các phản ví dụ cụ thể khi bị vi phạm.
  • Loại bỏ kết quả dương tính giả: Sử dụng tính năng theo dõi dữ liệu bị can thiệp qua 3 lần để cô lập các hàm tuỳ chỉnh chưa được liên kết, đảm bảo rằng các lỗi được báo cáo luôn có thể tái tạo.

Để xem phần giới thiệu và ví dụ thực tế, hãy xem bài đăng trên blog Nguồn mở của Google: Bảo mật kỷ nguyên dựa trên tác nhân: Giới thiệu quy trình xác minh chính thức cho CEL.