زبان عبارت مشترک (CEL) یک زبان عبارت عمومی است که برای سرعت، قابلیت حمل و اجرای ایمن طراحی شده است. میتوانید از CEL به تنهایی استفاده کنید یا آن را در یک محصول بزرگتر جاسازی کنید. CEL برای طیف گستردهای از برنامهها، از مسیریابی فراخوانیهای رویه از راه دور (RPC) گرفته تا تعریف سیاستهای امنیتی، بسیار مناسب است. CEL قابل توسعه، مستقل از پلتفرم، قابل تأیید رسمی و بهینه شده برای گردشهای کاری یکبار کامپایل/ارزیابی چندباره است.
CEL به طور خاص برای اجرای ایمن کد کاربر طراحی شده است. اگرچه فراخوانی کورکورانه eval() روی کد پایتون کاربر خطرناک است، اما میتوانید با خیال راحت کد CEL کاربر را اجرا کنید. و از آنجا که CEL از رفتاری که باعث کاهش عملکرد آن میشود جلوگیری میکند، ارزیابی را با خیال راحت در نانوثانیه یا میکروثانیه انجام میدهد. سرعت و ایمنی CEL آن را برای برنامههای کاربردی با عملکرد حیاتی ایدهآل میکند.
CEL عباراتی را ارزیابی میکند که مشابه توابع تکخطی یا عبارات لامبدا هستند. در حالی که CEL معمولاً برای تصمیمگیریهای بولی استفاده میشود، میتوانید از آن برای ساخت اشیاء پیچیدهتر مانند JSON یا پیامهای بافر پروتکل نیز استفاده کنید.
چرا سی ای ال؟
بسیاری از سرویسها و برنامهها پیکربندیهای اعلانی را ارزیابی میکنند. به عنوان مثال، کنترل دسترسی مبتنی بر نقش (RBAC) یک پیکربندی اعلانی است که با توجه به نقش کاربر و مجموعهای از کاربران، یک تصمیم دسترسی ایجاد میکند. در حالی که پیکربندیهای اعلانی برای اکثر موارد کافی هستند، گاهی اوقات به قدرت بیان بیشتری نیاز دارید. اینجاست که CEL وارد عمل میشود.
به عنوان مثالی از گسترش یک پیکربندی اعلانی با CEL، قابلیتهای مدیریت هویت و دسترسی گوگل کلود (IAM) را در نظر بگیرید. در حالی که RBAC مورد رایجی است، IAM عبارات CEL را ارائه میدهد تا به کاربران اجازه دهد دامنه اعطای مبتنی بر نقش را بر اساس ویژگیهای پیام اولیه درخواست یا منابع مورد دسترسی، بیشتر محدود کنند. توصیف چنین شرایطی از طریق مدل داده منجر به یک سطح API پیچیده میشود که کار با آن دشوار است. در عوض، استفاده از CEL با کنترل دسترسی مبتنی بر ویژگی (ABAC) یک گسترش رسا و قدرتمند برای RBAC است.
مفاهیم اصلی CEL
در CEL، یک عبارت در برابر یک محیط کامپایل میشود. مرحله کامپایل، یک درخت نحوی انتزاعی (AST) را در قالب بافر پروتکل تولید میکند. عبارات کامپایل شده برای استفادههای بعدی ذخیره میشوند تا ارزیابی تا حد امکان سریع باشد. یک عبارت کامپایل شده واحد را میتوان با ورودیهای مختلف زیادی ارزیابی کرد.
در اینجا نگاهی دقیقتر به برخی از این مفاهیم میاندازیم.
عبارات
عبارات توسط کاربران نوشته میشوند. عبارات مشابه بدنههای توابع تکخطی یا عبارات لامبدا هستند. امضای تابع که ورودی را اعلام میکند، خارج از عبارت CEL نوشته میشود و کتابخانه توابع موجود برای CEL به صورت خودکار وارد میشود.
برای مثال، عبارت CEL زیر یک شیء درخواست (request object) میگیرد و درخواست شامل یک توکن claims است. این عبارت یک مقدار بولی (boolean) برمیگرداند که نشان میدهد آیا توکن claims هنوز معتبر است یا خیر.
مثالی از عبارت CEL برای احراز هویت یک توکن claim
// 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 در سه مرحله پردازش میشوند:
- پارس کردن
- بررسی
- ارزیابی
رایجترین الگوی استفاده از CEL، تجزیه و بررسی عبارات در زمان پیکربندی، ذخیره AST و سپس بازیابی و ارزیابی مکرر AST در زمان اجرا است.
تصویرسازی مراحل پردازش CEL
CEL با استفاده از یک واژهپرداز و دستور زبان تجزیهکننده ANTLR از یک عبارت قابل خواندن توسط انسان به یک AST تجزیه میشود. مرحله تجزیه، یک AST مبتنی بر proto منتشر میکند که در آن هر گره Expr در AST حاوی یک شناسه عدد صحیح است که برای فهرستبندی در فرادادههای تولید شده در طول تجزیه و بررسی استفاده میشود. فایل syntax.proto که در طول تجزیه تولید میشود، نمایش انتزاعی از آنچه در فرم رشتهای عبارت تایپ شده است را نشان میدهد.
پس از تجزیه یک عبارت، آن را در برابر محیط بررسی نوع میکنند تا اطمینان حاصل شود که تمام شناسههای متغیر و تابع در عبارت به درستی تعریف شده و مورد استفاده قرار میگیرند. بررسی نوع، یک فایل checked.proto تولید میکند که شامل ابردادههای مربوط به تفکیک نوع، متغیر و تابع است که میتواند کارایی ارزیابی را به طور چشمگیری بهبود بخشد.
در نهایت، پس از تجزیه و بررسی یک عبارت، AST ذخیره شده ارزیابی میشود.
ارزیاب CEL به سه چیز نیاز دارد:
- اتصال توابع برای هرگونه افزونه سفارشی
- اتصال متغیرها
- یک AST برای ارزیابی
اتصالات تابع و متغیر باید با آنچه برای کامپایل AST استفاده شده است، مطابقت داشته باشند. هر یک از این ورودیها را میتوان در ارزیابیهای متعدد مورد استفاده مجدد قرار داد، مانند ارزیابی یک AST در میان مجموعههای زیادی از اتصالات متغیر، استفاده از متغیرهای یکسان در برابر بسیاری از ASTها، یا اتصالات تابع مورد استفاده در طول عمر یک فرآیند (یک مورد رایج).
تأیید رسمی
علاوه بر ارزیابی زمان اجرا، عبارات و سیاستهای CEL را میتوان به صورت رسمی تأیید کرد تا صحت آنها در تمام ورودیهای ممکن به صورت ریاضی اثبات شود.
چارچوب تأیید رسمی CEL در CEL-Java که با استفاده از اثباتکننده قضیه Z3 ارائه میشود، عبارات و سیاستهای CEL را به فرمولهای نظریههای مدول رضایتبخشی (SMT) تبدیل میکند تا:
- اثبات متغیرهای امنیتی: با استفاده از مشخصات
assumeوassertتأیید کنید که سیاستهای حیاتی تحت هیچ ترکیبی از ورودیها قابل دور زدن نیستند. - تأیید همارزی منطقی: به صورت ریاضی ثابت کنید که عبارات بازسازیشده یا تولیدشده توسط هوش مصنوعی، رفتاری یکسان با قانون اصلی دارند.
- اعتبار جامع را اعمال کنید: تضمین کنید که گاردریلها (مانند سیاستهای پذیرش اعتبارسنجی Kubernetes) در تمام ورودیها رعایت شوند، یا در صورت نقض، مثالهای نقض مشخصی ایجاد کنید.
- حذف موارد مثبت کاذب: از ردیابی سه مرحلهای برای جداسازی توابع سفارشی نگاشت نشده استفاده کنید و اطمینان حاصل کنید که تخلفات گزارش شده همیشه اشکالات قابل تکرار هستند.
برای مقدمه و مثالهای دنیای واقعی، به پست وبلاگ منبع باز گوگل با عنوان « ایمنسازی دوران عاملیت: معرفی تأیید رسمی برای CEL» مراجعه کنید.
منابع مرتبط
،زبان عبارت مشترک (CEL) یک زبان عبارت عمومی است که برای سرعت، قابلیت حمل و اجرای ایمن طراحی شده است. میتوانید از CEL به تنهایی استفاده کنید یا آن را در یک محصول بزرگتر جاسازی کنید. CEL برای طیف گستردهای از برنامهها، از مسیریابی فراخوانیهای رویه از راه دور (RPC) گرفته تا تعریف سیاستهای امنیتی، بسیار مناسب است. CEL قابل توسعه، مستقل از پلتفرم، قابل تأیید رسمی و بهینه شده برای گردشهای کاری یکبار کامپایل/ارزیابی چندباره است.
CEL به طور خاص برای اجرای ایمن کد کاربر طراحی شده است. اگرچه فراخوانی کورکورانه eval() روی کد پایتون کاربر خطرناک است، اما میتوانید با خیال راحت کد CEL کاربر را اجرا کنید. و از آنجا که CEL از رفتاری که باعث کاهش عملکرد آن میشود جلوگیری میکند، ارزیابی را با خیال راحت در نانوثانیه یا میکروثانیه انجام میدهد. سرعت و ایمنی CEL آن را برای برنامههای کاربردی با عملکرد حیاتی ایدهآل میکند.
CEL عباراتی را ارزیابی میکند که مشابه توابع تکخطی یا عبارات لامبدا هستند. در حالی که CEL معمولاً برای تصمیمگیریهای بولی استفاده میشود، میتوانید از آن برای ساخت اشیاء پیچیدهتر مانند JSON یا پیامهای بافر پروتکل نیز استفاده کنید.
چرا سی ای ال؟
بسیاری از سرویسها و برنامهها پیکربندیهای اعلانی را ارزیابی میکنند. به عنوان مثال، کنترل دسترسی مبتنی بر نقش (RBAC) یک پیکربندی اعلانی است که با توجه به نقش کاربر و مجموعهای از کاربران، یک تصمیم دسترسی ایجاد میکند. در حالی که پیکربندیهای اعلانی برای اکثر موارد کافی هستند، گاهی اوقات به قدرت بیان بیشتری نیاز دارید. اینجاست که CEL وارد عمل میشود.
به عنوان مثالی از گسترش یک پیکربندی اعلانی با CEL، قابلیتهای مدیریت هویت و دسترسی گوگل کلود (IAM) را در نظر بگیرید. در حالی که RBAC مورد رایجی است، IAM عبارات CEL را ارائه میدهد تا به کاربران اجازه دهد دامنه اعطای مبتنی بر نقش را بر اساس ویژگیهای پیام اولیه درخواست یا منابع مورد دسترسی، بیشتر محدود کنند. توصیف چنین شرایطی از طریق مدل داده منجر به یک سطح API پیچیده میشود که کار با آن دشوار است. در عوض، استفاده از CEL با کنترل دسترسی مبتنی بر ویژگی (ABAC) یک گسترش رسا و قدرتمند برای RBAC است.
مفاهیم اصلی CEL
در CEL، یک عبارت در برابر یک محیط کامپایل میشود. مرحله کامپایل، یک درخت نحوی انتزاعی (AST) را در قالب بافر پروتکل تولید میکند. عبارات کامپایل شده برای استفادههای بعدی ذخیره میشوند تا ارزیابی تا حد امکان سریع باشد. یک عبارت کامپایل شده واحد را میتوان با ورودیهای مختلف زیادی ارزیابی کرد.
در اینجا نگاهی دقیقتر به برخی از این مفاهیم میاندازیم.
عبارات
عبارات توسط کاربران نوشته میشوند. عبارات مشابه بدنههای توابع تکخطی یا عبارات لامبدا هستند. امضای تابع که ورودی را اعلام میکند، خارج از عبارت CEL نوشته میشود و کتابخانه توابع موجود برای CEL به صورت خودکار وارد میشود.
برای مثال، عبارت CEL زیر یک شیء درخواست (request object) میگیرد و درخواست شامل یک توکن claims است. این عبارت یک مقدار بولی (boolean) برمیگرداند که نشان میدهد آیا توکن claims هنوز معتبر است یا خیر.
مثالی از عبارت CEL برای احراز هویت یک توکن claim
// 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 در سه مرحله پردازش میشوند:
- پارس کردن
- بررسی
- ارزیابی
رایجترین الگوی استفاده از CEL، تجزیه و بررسی عبارات در زمان پیکربندی، ذخیره AST و سپس بازیابی و ارزیابی مکرر AST در زمان اجرا است.
تصویرسازی مراحل پردازش CEL
CEL با استفاده از یک واژهپرداز و دستور زبان تجزیهکننده ANTLR از یک عبارت قابل خواندن توسط انسان به یک AST تجزیه میشود. مرحله تجزیه، یک AST مبتنی بر proto منتشر میکند که در آن هر گره Expr در AST حاوی یک شناسه عدد صحیح است که برای فهرستبندی در فرادادههای تولید شده در طول تجزیه و بررسی استفاده میشود. فایل syntax.proto که در طول تجزیه تولید میشود، نمایش انتزاعی از آنچه در فرم رشتهای عبارت تایپ شده است را نشان میدهد.
پس از تجزیه یک عبارت، آن را در برابر محیط بررسی نوع میکنند تا اطمینان حاصل شود که تمام شناسههای متغیر و تابع در عبارت به درستی تعریف شده و مورد استفاده قرار میگیرند. بررسی نوع، یک فایل checked.proto تولید میکند که شامل ابردادههای مربوط به تفکیک نوع، متغیر و تابع است که میتواند کارایی ارزیابی را به طور چشمگیری بهبود بخشد.
در نهایت، پس از تجزیه و بررسی یک عبارت، AST ذخیره شده ارزیابی میشود.
ارزیاب CEL به سه چیز نیاز دارد:
- اتصال توابع برای هرگونه افزونه سفارشی
- اتصال متغیرها
- یک AST برای ارزیابی
اتصالات تابع و متغیر باید با آنچه برای کامپایل AST استفاده شده است، مطابقت داشته باشند. هر یک از این ورودیها را میتوان در ارزیابیهای متعدد مورد استفاده مجدد قرار داد، مانند ارزیابی یک AST در میان مجموعههای زیادی از اتصالات متغیر، استفاده از متغیرهای یکسان در برابر بسیاری از ASTها، یا اتصالات تابع مورد استفاده در طول عمر یک فرآیند (یک مورد رایج).
تأیید رسمی
علاوه بر ارزیابی زمان اجرا، عبارات و سیاستهای CEL را میتوان به صورت رسمی تأیید کرد تا صحت آنها در تمام ورودیهای ممکن به صورت ریاضی اثبات شود.
چارچوب تأیید رسمی CEL در CEL-Java که با استفاده از اثباتکننده قضیه Z3 ارائه میشود، عبارات و سیاستهای CEL را به فرمولهای نظریههای مدول رضایتبخشی (SMT) تبدیل میکند تا:
- اثبات متغیرهای امنیتی: با استفاده از مشخصات
assumeوassertتأیید کنید که سیاستهای حیاتی تحت هیچ ترکیبی از ورودیها قابل دور زدن نیستند. - تأیید همارزی منطقی: به صورت ریاضی ثابت کنید که عبارات بازسازیشده یا تولیدشده توسط هوش مصنوعی، رفتاری یکسان با قانون اصلی دارند.
- اعتبار جامع را اعمال کنید: تضمین کنید که گاردریلها (مانند سیاستهای پذیرش اعتبارسنجی Kubernetes) در تمام ورودیها رعایت شوند، یا در صورت نقض، مثالهای نقض مشخصی ایجاد کنید.
- حذف موارد مثبت کاذب: از ردیابی سه مرحلهای برای جداسازی توابع سفارشی نگاشت نشده استفاده کنید و اطمینان حاصل کنید که تخلفات گزارش شده همیشه اشکالات قابل تکرار هستند.
برای مقدمه و مثالهای دنیای واقعی، به پست وبلاگ منبع باز گوگل با عنوان « ایمنسازی دوران عاملیت: معرفی تأیید رسمی برای CEL» مراجعه کنید.
منابع مرتبط
،زبان عبارت مشترک (CEL) یک زبان عبارت عمومی است که برای سرعت، قابلیت حمل و اجرای ایمن طراحی شده است. میتوانید از CEL به تنهایی استفاده کنید یا آن را در یک محصول بزرگتر جاسازی کنید. CEL برای طیف گستردهای از برنامهها، از مسیریابی فراخوانیهای رویه از راه دور (RPC) گرفته تا تعریف سیاستهای امنیتی، بسیار مناسب است. CEL قابل توسعه، مستقل از پلتفرم، قابل تأیید رسمی و بهینه شده برای گردشهای کاری یکبار کامپایل/ارزیابی چندباره است.
CEL به طور خاص برای اجرای ایمن کد کاربر طراحی شده است. اگرچه فراخوانی کورکورانه eval() روی کد پایتون کاربر خطرناک است، اما میتوانید با خیال راحت کد CEL کاربر را اجرا کنید. و از آنجا که CEL از رفتاری که باعث کاهش عملکرد آن میشود جلوگیری میکند، ارزیابی را با خیال راحت در نانوثانیه یا میکروثانیه انجام میدهد. سرعت و ایمنی CEL آن را برای برنامههای کاربردی با عملکرد حیاتی ایدهآل میکند.
CEL عباراتی را ارزیابی میکند که مشابه توابع تکخطی یا عبارات لامبدا هستند. در حالی که CEL معمولاً برای تصمیمگیریهای بولی استفاده میشود، میتوانید از آن برای ساخت اشیاء پیچیدهتر مانند JSON یا پیامهای بافر پروتکل نیز استفاده کنید.
چرا سی ای ال؟
بسیاری از سرویسها و برنامهها پیکربندیهای اعلانی را ارزیابی میکنند. به عنوان مثال، کنترل دسترسی مبتنی بر نقش (RBAC) یک پیکربندی اعلانی است که با توجه به نقش کاربر و مجموعهای از کاربران، یک تصمیم دسترسی ایجاد میکند. در حالی که پیکربندیهای اعلانی برای اکثر موارد کافی هستند، گاهی اوقات به قدرت بیان بیشتری نیاز دارید. اینجاست که CEL وارد عمل میشود.
به عنوان مثالی از گسترش یک پیکربندی اعلانی با CEL، قابلیتهای مدیریت هویت و دسترسی گوگل کلود (IAM) را در نظر بگیرید. در حالی که RBAC مورد رایجی است، IAM عبارات CEL را ارائه میدهد تا به کاربران اجازه دهد دامنه اعطای مبتنی بر نقش را بر اساس ویژگیهای پیام اولیه درخواست یا منابع مورد دسترسی، بیشتر محدود کنند. توصیف چنین شرایطی از طریق مدل داده منجر به یک سطح API پیچیده میشود که کار با آن دشوار است. در عوض، استفاده از CEL با کنترل دسترسی مبتنی بر ویژگی (ABAC) یک گسترش رسا و قدرتمند برای RBAC است.
مفاهیم اصلی CEL
در CEL، یک عبارت در برابر یک محیط کامپایل میشود. مرحله کامپایل، یک درخت نحوی انتزاعی (AST) را در قالب بافر پروتکل تولید میکند. عبارات کامپایل شده برای استفادههای بعدی ذخیره میشوند تا ارزیابی تا حد امکان سریع باشد. یک عبارت کامپایل شده واحد را میتوان با ورودیهای مختلف زیادی ارزیابی کرد.
در اینجا نگاهی دقیقتر به برخی از این مفاهیم میاندازیم.
عبارات
عبارات توسط کاربران نوشته میشوند. عبارات مشابه بدنههای توابع تکخطی یا عبارات لامبدا هستند. امضای تابع که ورودی را اعلام میکند، خارج از عبارت CEL نوشته میشود و کتابخانه توابع موجود برای CEL به صورت خودکار وارد میشود.
برای مثال، عبارت CEL زیر یک شیء درخواست (request object) میگیرد و درخواست شامل یک توکن claims است. این عبارت یک مقدار بولی (boolean) برمیگرداند که نشان میدهد آیا توکن claims هنوز معتبر است یا خیر.
مثالی از عبارت CEL برای احراز هویت یک توکن claim
// 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 در سه مرحله پردازش میشوند:
- پارس کردن
- بررسی
- ارزیابی
رایجترین الگوی استفاده از CEL، تجزیه و بررسی عبارات در زمان پیکربندی، ذخیره AST و سپس بازیابی و ارزیابی مکرر AST در زمان اجرا است.
تصویرسازی مراحل پردازش CEL
CEL با استفاده از یک واژهپرداز و دستور زبان تجزیهکننده ANTLR از یک عبارت قابل خواندن توسط انسان به یک AST تجزیه میشود. مرحله تجزیه، یک AST مبتنی بر proto منتشر میکند که در آن هر گره Expr در AST حاوی یک شناسه عدد صحیح است که برای فهرستبندی در فرادادههای تولید شده در طول تجزیه و بررسی استفاده میشود. فایل syntax.proto که در طول تجزیه تولید میشود، نمایش انتزاعی از آنچه در فرم رشتهای عبارت تایپ شده است را نشان میدهد.
پس از تجزیه یک عبارت، آن را در برابر محیط بررسی نوع میکنند تا اطمینان حاصل شود که تمام شناسههای متغیر و تابع در عبارت به درستی تعریف شده و مورد استفاده قرار میگیرند. بررسی نوع، یک فایل checked.proto تولید میکند که شامل ابردادههای مربوط به تفکیک نوع، متغیر و تابع است که میتواند کارایی ارزیابی را به طور چشمگیری بهبود بخشد.
در نهایت، پس از تجزیه و بررسی یک عبارت، AST ذخیره شده ارزیابی میشود.
ارزیاب CEL به سه چیز نیاز دارد:
- اتصال توابع برای هرگونه افزونه سفارشی
- اتصال متغیرها
- یک AST برای ارزیابی
اتصالات تابع و متغیر باید با آنچه برای کامپایل AST استفاده شده است، مطابقت داشته باشند. هر یک از این ورودیها را میتوان در ارزیابیهای متعدد مورد استفاده مجدد قرار داد، مانند ارزیابی یک AST در میان مجموعههای زیادی از اتصالات متغیر، استفاده از متغیرهای یکسان در برابر بسیاری از ASTها، یا اتصالات تابع مورد استفاده در طول عمر یک فرآیند (یک مورد رایج).
تأیید رسمی
علاوه بر ارزیابی زمان اجرا، عبارات و سیاستهای CEL را میتوان به صورت رسمی تأیید کرد تا صحت آنها در تمام ورودیهای ممکن به صورت ریاضی اثبات شود.
چارچوب تأیید رسمی CEL در CEL-Java که با استفاده از اثباتکننده قضیه Z3 ارائه میشود، عبارات و سیاستهای CEL را به فرمولهای نظریههای مدول رضایتبخشی (SMT) تبدیل میکند تا:
- اثبات متغیرهای امنیتی: با استفاده از مشخصات
assumeوassertتأیید کنید که سیاستهای حیاتی تحت هیچ ترکیبی از ورودیها قابل دور زدن نیستند. - تأیید همارزی منطقی: به صورت ریاضی ثابت کنید که عبارات بازسازیشده یا تولیدشده توسط هوش مصنوعی، رفتاری یکسان با قانون اصلی دارند.
- اعتبار جامع را اعمال کنید: تضمین کنید که گاردریلها (مانند سیاستهای پذیرش اعتبارسنجی Kubernetes) در تمام ورودیها رعایت شوند، یا در صورت نقض، مثالهای نقض مشخصی ایجاد کنید.
- حذف موارد مثبت کاذب: از ردیابی سه مرحلهای برای جداسازی توابع سفارشی نگاشت نشده استفاده کنید و اطمینان حاصل کنید که تخلفات گزارش شده همیشه اشکالات قابل تکرار هستند.
برای مقدمه و مثالهای دنیای واقعی، به پست وبلاگ منبع باز گوگل با عنوان « ایمنسازی دوران عاملیت: معرفی تأیید رسمی برای CEL» مراجعه کنید.
منابع مرتبط
،زبان عبارت مشترک (CEL) یک زبان عبارت عمومی است که برای سرعت، قابلیت حمل و اجرای ایمن طراحی شده است. میتوانید از CEL به تنهایی استفاده کنید یا آن را در یک محصول بزرگتر جاسازی کنید. CEL برای طیف گستردهای از برنامهها، از مسیریابی فراخوانیهای رویه از راه دور (RPC) گرفته تا تعریف سیاستهای امنیتی، بسیار مناسب است. CEL قابل توسعه، مستقل از پلتفرم، قابل تأیید رسمی و بهینه شده برای گردشهای کاری یکبار کامپایل/ارزیابی چندباره است.
CEL به طور خاص برای اجرای ایمن کد کاربر طراحی شده است. اگرچه فراخوانی کورکورانه eval() روی کد پایتون کاربر خطرناک است، اما میتوانید با خیال راحت کد CEL کاربر را اجرا کنید. و از آنجا که CEL از رفتاری که باعث کاهش عملکرد آن میشود جلوگیری میکند، ارزیابی را با خیال راحت در نانوثانیه یا میکروثانیه انجام میدهد. سرعت و ایمنی CEL آن را برای برنامههای کاربردی با عملکرد حیاتی ایدهآل میکند.
CEL عباراتی را ارزیابی میکند که مشابه توابع تکخطی یا عبارات لامبدا هستند. در حالی که CEL معمولاً برای تصمیمگیریهای بولی استفاده میشود، میتوانید از آن برای ساخت اشیاء پیچیدهتر مانند JSON یا پیامهای بافر پروتکل نیز استفاده کنید.
چرا سی ای ال؟
بسیاری از سرویسها و برنامهها پیکربندیهای اعلانی را ارزیابی میکنند. به عنوان مثال، کنترل دسترسی مبتنی بر نقش (RBAC) یک پیکربندی اعلانی است که با توجه به نقش کاربر و مجموعهای از کاربران، یک تصمیم دسترسی ایجاد میکند. در حالی که پیکربندیهای اعلانی برای اکثر موارد کافی هستند، گاهی اوقات به قدرت بیان بیشتری نیاز دارید. اینجاست که CEL وارد عمل میشود.
به عنوان مثالی از گسترش یک پیکربندی اعلانی با CEL، قابلیتهای مدیریت هویت و دسترسی گوگل کلود (IAM) را در نظر بگیرید. در حالی که RBAC مورد رایجی است، IAM عبارات CEL را ارائه میدهد تا به کاربران اجازه دهد دامنه اعطای مبتنی بر نقش را بر اساس ویژگیهای پیام اولیه درخواست یا منابع مورد دسترسی، بیشتر محدود کنند. توصیف چنین شرایطی از طریق مدل داده منجر به یک سطح API پیچیده میشود که کار با آن دشوار است. در عوض، استفاده از CEL با کنترل دسترسی مبتنی بر ویژگی (ABAC) یک گسترش رسا و قدرتمند برای RBAC است.
مفاهیم اصلی CEL
در CEL، یک عبارت در برابر یک محیط کامپایل میشود. مرحله کامپایل، یک درخت نحوی انتزاعی (AST) را در قالب بافر پروتکل تولید میکند. عبارات کامپایل شده برای استفادههای بعدی ذخیره میشوند تا ارزیابی تا حد امکان سریع باشد. یک عبارت کامپایل شده واحد را میتوان با ورودیهای مختلف زیادی ارزیابی کرد.
در اینجا نگاهی دقیقتر به برخی از این مفاهیم میاندازیم.
عبارات
عبارات توسط کاربران نوشته میشوند. عبارات مشابه بدنههای توابع تکخطی یا عبارات لامبدا هستند. امضای تابع که ورودی را اعلام میکند، خارج از عبارت CEL نوشته میشود و کتابخانه توابع موجود برای CEL به صورت خودکار وارد میشود.
برای مثال، عبارت CEL زیر یک شیء درخواست (request object) میگیرد و درخواست شامل یک توکن claims است. این عبارت یک مقدار بولی (boolean) برمیگرداند که نشان میدهد آیا توکن claims هنوز معتبر است یا خیر.
مثالی از عبارت CEL برای احراز هویت یک توکن claim
// 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 در سه مرحله پردازش میشوند:
- پارس کردن
- بررسی
- ارزیابی
رایجترین الگوی استفاده از CEL، تجزیه و بررسی عبارات در زمان پیکربندی، ذخیره AST و سپس بازیابی و ارزیابی مکرر AST در زمان اجرا است.
تصویرسازی مراحل پردازش CEL
CEL با استفاده از یک واژهپرداز و دستور زبان تجزیهکننده ANTLR از یک عبارت قابل خواندن توسط انسان به یک AST تجزیه میشود. مرحله تجزیه، یک AST مبتنی بر proto منتشر میکند که در آن هر گره Expr در AST حاوی یک شناسه عدد صحیح است که برای فهرستبندی در فرادادههای تولید شده در طول تجزیه و بررسی استفاده میشود. فایل syntax.proto که در طول تجزیه تولید میشود، نمایش انتزاعی از آنچه در فرم رشتهای عبارت تایپ شده است را نشان میدهد.
پس از تجزیه یک عبارت، آن را در برابر محیط بررسی نوع میکنند تا اطمینان حاصل شود که تمام شناسههای متغیر و تابع در عبارت به درستی تعریف شده و مورد استفاده قرار میگیرند. بررسی نوع، یک فایل checked.proto تولید میکند که شامل ابردادههای مربوط به تفکیک نوع، متغیر و تابع است که میتواند کارایی ارزیابی را به طور چشمگیری بهبود بخشد.
در نهایت، پس از تجزیه و بررسی یک عبارت، AST ذخیره شده ارزیابی میشود.
ارزیاب CEL به سه چیز نیاز دارد:
- اتصال توابع برای هرگونه افزونه سفارشی
- اتصال متغیرها
- یک AST برای ارزیابی
اتصالات تابع و متغیر باید با آنچه برای کامپایل AST استفاده شده است، مطابقت داشته باشند. هر یک از این ورودیها را میتوان در ارزیابیهای متعدد مورد استفاده مجدد قرار داد، مانند ارزیابی یک AST در میان مجموعههای زیادی از اتصالات متغیر، استفاده از متغیرهای یکسان در برابر بسیاری از ASTها، یا اتصالات تابع مورد استفاده در طول عمر یک فرآیند (یک مورد رایج).
تأیید رسمی
علاوه بر ارزیابی زمان اجرا، عبارات و سیاستهای CEL را میتوان به صورت رسمی تأیید کرد تا صحت آنها در تمام ورودیهای ممکن به صورت ریاضی اثبات شود.
چارچوب تأیید رسمی CEL در CEL-Java که با استفاده از اثباتکننده قضیه Z3 ارائه میشود، عبارات و سیاستهای CEL را به فرمولهای نظریههای مدول رضایتبخشی (SMT) تبدیل میکند تا:
- اثبات متغیرهای امنیتی: با استفاده از مشخصات
assumeوassertتأیید کنید که سیاستهای حیاتی تحت هیچ ترکیبی از ورودیها قابل دور زدن نیستند. - تأیید همارزی منطقی: به صورت ریاضی ثابت کنید که عبارات بازسازیشده یا تولیدشده توسط هوش مصنوعی، رفتاری یکسان با قانون اصلی دارند.
- اعتبار جامع را اعمال کنید: تضمین کنید که گاردریلها (مانند سیاستهای پذیرش اعتبارسنجی Kubernetes) در تمام ورودیها رعایت شوند، یا در صورت نقض، مثالهای نقض مشخصی ایجاد کنید.
- حذف موارد مثبت کاذب: از ردیابی سه مرحلهای برای جداسازی توابع سفارشی نگاشت نشده استفاده کنید و اطمینان حاصل کنید که تخلفات گزارش شده همیشه اشکالات قابل تکرار هستند.
برای مقدمه و مثالهای دنیای واقعی، به پست وبلاگ منبع باز گوگل با عنوان « ایمنسازی دوران عاملیت: معرفی تأیید رسمی برای CEL» مراجعه کنید.