ภาษาของนิพจน์ทั่วไป (CEL)

Common Expression Language (CEL) เป็นภาษาสำหรับนิพจน์อเนกประสงค์ที่ออกแบบมาให้รวดเร็ว พกพาสะดวก และปลอดภัยในการดำเนินการ คุณสามารถใช้ CEL ด้วยตัวเองหรือฝังไว้ในผลิตภัณฑ์ขนาดใหญ่กว่า CEL เหมาะอย่างยิ่งสำหรับแอปพลิเคชันที่หลากหลาย ตั้งแต่การกำหนดเส้นทางการเรียกใช้โพรซีเยอร์ระยะไกล (RPC) ไปจนถึงการกำหนดนโยบายความปลอดภัย CEL ขยายได้ ไม่ขึ้นกับแพลตฟอร์ม ตรวจสอบได้อย่างเป็นทางการ และเพิ่มประสิทธิภาพสำหรับเวิร์กโฟลว์การคอมไพล์ 1 ครั้ง/ประเมินหลายครั้ง

CEL ได้รับการออกแบบมาโดยเฉพาะให้ปลอดภัยสำหรับการดำเนินการโค้ดของผู้ใช้ แม้ว่าการเรียกใช้ eval() ในโค้ด Python ของผู้ใช้โดยไม่ตรวจสอบจะอันตราย แต่คุณสามารถดำเนินการโค้ด CEL ของผู้ใช้ได้อย่างปลอดภัย และเนื่องจาก CEL ป้องกันไม่ให้เกิดพฤติกรรมที่จะทำให้ประสิทธิภาพลดลง จึงประเมินได้อย่างปลอดภัยในระดับนาโนวินาทีหรือไมโครวินาที ความเร็วและความปลอดภัยของ CEL ทำให้ภาษาดังกล่าวเหมาะอย่างยิ่งสำหรับแอปพลิเคชันที่สำคัญต่อประสิทธิภาพ

CEL จะประเมินนิพจน์ที่คล้ายกับฟังก์ชันบรรทัดเดียวหรือนิพจน์แลมดา แม้ว่าโดยทั่วไปจะใช้ CEL สำหรับการตัดสินใจแบบบูลีน แต่คุณก็ยังใช้ CEL เพื่อสร้างออบเจ็กต์ที่ซับซ้อนมากขึ้น เช่น ข้อความ JSON หรือบัฟเฟอร์โปรโตคอลได้ด้วย

เหตุใดจึงควรใช้ 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 สำหรับการตรวจสอบสิทธิ์โทเค็น 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

แม้ว่าผู้ใช้จะเป็นผู้กำหนดนิพจน์ 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 ใน 3 ระยะ ได้แก่

1. แยกวิเคราะห์
2. ตรวจสอบ
3. ประเมิน

รูปแบบการใช้งาน CEL ที่พบบ่อยที่สุดคือการแยกวิเคราะห์และตรวจสอบนิพจน์ในเวลาที่กำหนดค่า จัดเก็บ AST แล้วดึงและประเมิน AST ซ้ำๆ ในเวลาที่รัน

ภาพประกอบระยะการประมวลผล CEL

ระบบจะแยกวิเคราะห์ CEL จากนิพจน์ที่มนุษย์อ่านได้เป็น AST โดยใช้ไวยากรณ์ของตัวแยกคำและตัวแยกวิเคราะห์ ANTLR ระยะการแยกวิเคราะห์จะสร้าง AST ตามโปรโต ซึ่งโหนด Expr แต่ละโหนดใน AST จะมีรหัสจำนวนเต็มที่ใช้ในการ จัดทำดัชนีข้อมูลเมตาที่สร้างขึ้นระหว่างการแยกวิเคราะห์และการตรวจสอบ ไฟล์ syntax.proto ที่สร้างขึ้นระหว่างการแยกวิเคราะห์แสดงถึง การแสดงนามธรรมของสิ่งที่พิมพ์ในรูปแบบสตริงของ นิพจน์

หลังจากแยกวิเคราะห์นิพจน์แล้ว ระบบจะตรวจสอบประเภทนิพจน์กับสภาพแวดล้อมเพื่อให้แน่ใจว่ามีการประกาศตัวระบุตัวแปรและฟังก์ชันทั้งหมดในนิพจน์และมีการใช้งานอย่างถูกต้อง ตัวตรวจสอบประเภทจะสร้างไฟล์ checked.protoซึ่งมีข้อมูลเมตาการแก้ปัญหาประเภท ตัวแปร และฟังก์ชัน ซึ่งจะช่วยเพิ่มประสิทธิภาพการประเมินได้อย่างมาก

สุดท้าย หลังจากแยกวิเคราะห์และตรวจสอบนิพจน์แล้ว ระบบจะประเมิน AST ที่จัดเก็บไว้

ตัวประเมิน CEL ต้องการสิ่งต่อไปนี้ 3 อย่าง

• การเชื่อมโยงฟังก์ชันสำหรับส่วนขยายที่กำหนดเอง
• การเชื่อมโยงตัวแปร
• AST ที่จะประเมิน

การเชื่อมโยงฟังก์ชันและตัวแปรควรตรงกับสิ่งที่ใช้ในการคอมไพล์ AST คุณสามารถนำอินพุตเหล่านี้ไปใช้ซ้ำในการประเมินหลายครั้งได้ เช่น การประเมิน AST ในชุดการเชื่อมโยงตัวแปรหลายชุด การใช้ตัวแปรเดียวกันกับ AST หลายรายการ หรือการใช้การเชื่อมโยงฟังก์ชันตลอดอายุการใช้งานของกระบวนการ (กรณีทั่วไป)

การตรวจสอบอย่างเป็นทางการ

นอกจากการประเมินรันไทม์แล้ว คุณยังตรวจสอบอย่างเป็นทางการ นิพจน์และนโยบาย CEL เพื่อพิสูจน์ความถูกต้องทางคณิตศาสตร์ในอินพุตที่เป็นไปได้ทั้งหมดได้ด้วย

เฟรมเวิร์กการตรวจสอบอย่างเป็นทางการของ CEL Framework ใน CEL-Java ซึ่งขับเคลื่อนโดยตัวพิสูจน์ทฤษฎีบท Z3 theorem prover จะแปลนิพจน์และ CEL Policies เป็นสูตร Satisfiability Modulo Theories (SMT) เพื่อดำเนินการต่อไปนี้

• พิสูจน์ตัวแปรความปลอดภัย: ตรวจสอบว่าไม่สามารถข้ามผ่านนโยบายที่สำคัญได้ภายใต้การรวมอินพุตใดๆ โดยใช้ข้อกำหนด assume และ assert
• ตรวจสอบความสมมูลเชิงตรรกะ: พิสูจน์ทางคณิตศาสตร์ว่านิพจน์ที่ปรับโครงสร้างใหม่หรือนิพจน์ที่ AI สร้างขึ้นทำงานเหมือนกับกฎเดิม
• บังคับใช้ความถูกต้องที่ครอบคลุม: รับประกันว่าการ์ดเรล (เช่น นโยบายการยอมรับการตรวจสอบของ Kubernetes) จะมีผลกับอินพุตทั้งหมด หรือสร้างตัวอย่างที่ขัดแย้งที่เป็นรูปธรรมเมื่อมีการละเมิด
• กำจัดผลลบลวง: ใช้การติดตามการปนเปื้อน 3 รอบเพื่อแยกฟังก์ชันที่กำหนดเองซึ่งไม่ได้แมป เพื่อให้แน่ใจว่าการละเมิดที่รายงานเป็นข้อบกพร่องที่ทำซ้ำได้เสมอ

หากต้องการดูข้อมูลเบื้องต้นและตัวอย่างการใช้งานจริง โปรดดูโพสต์ในบล็อก Google Open Source เรื่อง Securing the agentic era: Introducing formal verification for CEL

แหล่งข้อมูลที่เกี่ยวข้อง

• บทแนะนำ CEL
• คำจำกัดความของภาษา
• คู่มืออ้างอิงฟังก์ชัน
• ประกาศการตรวจสอบอย่างเป็นทางการ
• ที่เก็บตัวตรวจสอบ CEL Java