Cổng Kiểm soát Xác minh Chính thức: Giải pháp Nâng cao An toàn cho AI Lập trình Mã nguồn

Một số lỗi phần mềm nghiêm trọng nhất thực chất lại khá nhàm chán. Một người dùng không được phép đọc dữ liệu của người dùng khác. Không ai phản bác điều này, và trong các buổi xem xét thiết kế, chẳng ai đứng lên bảo vệ quyền của Alice khi cô ấy đọc hồ sơ của Bob. Tuy nhiên, lỗi kiểm soát truy cập (broken access control) vẫn luôn đứng đầu danh sách OWASP Top 10.

Những lỗi này xuất hiện vì quy tắc đã được đặt sai vị trí trong hệ thống. Nó nằm trong một prompt, trong danh sách kiểm tra (checklist), hoặc dựa trên kỳ vọng rằng mọi kỹ sư tương lai — và giờ là mọi lần gọi mô hình AI — sẽ nhớ nguyên tắc bất biến đó và áp dụng lại đúng cách.

Giả định này vốn đã yếu ớt, và khi AI tạo ra phần lớn mã nguồn, nó hoàn toàn sụp đổ. Bạn có thể làm tất cả những điều hiển nhiên: đặt quy tắc vào tệp CLAUDE.md, viết system prompt cẩn thận, thêm dòng chữ "ủy quyền RẤT QUAN TRỌNG" vào hướng dẫn cho tác nhân AI. Bạn nên làm những điều đó. Nhưng sau khi mô hình viết ra mười sáu ngàn dòng mã, câu hỏi thực sự vẫn còn lại: Làm sao bạn biết mã đó làm đúng những gì bạn muốn?

Kiểm thử (test) có giúp ích, nhưng kiểm thử mang tính thực nghiệm. Nó kiểm tra các trường hợp mà bạn và mô hình nhớ ra để viết, nhưng nó không thể nói lên gì về trình xử lý mà ai đó sẽ thêm vào tuần tới.

Minh họa vòng lặp kiểm soát

Cổng hành vi so với Cổng cấu trúc

Hầu hết các ràng buộc ở mức prompt đều là "cổng hành vi" (behavioral gates). Chúng ta bảo mô hình "đừng bỏ qua ủy quyền", "hãy xác thực đầu vào", "dùng hàm trợ giúp chung". Mô hình tuân theo các hướng dẫn này đủ thường để trở nên hữu ích, nhưng cũng thất bại đủ thường để khiến toàn bộ sự sắp xếp trở nên mất ổn định. Cổng hành vi phụ thuộc vào việc mô hình nhớ quy tắc, nhận ra nơi áp dụng, chống lại sự lôi cuốn của ngữ cảnh cục bộ, và sau đó là người xem xét duy trì nguyên tắc bất biến đó trên toàn bộ cơ sở mã.

"Cổng cấu trúc" (structural gates) thì khác. Một trình biên dịch, bộ kiểm tra kiểu (type checker), trình chạy kiểm thử, bộ làm sạch mã (linter), hay bộ kiểm tra chứng minh. Mỗi cái tạo ra một câu trả lời cụ thể về hiện vật (artifact) trước mặt nó. Câu trả lời không hoàn hảo, nhưng nó là thật, và trong phạm vi của nó, nó từ chối khi mã sai.

Sự từ chối đó chính là điểm mấu chốt. Nó cho phép chúng ta chuyển công việc ra khỏi không gian hướng dẫn của mô hình và vào nền tảng (substrate) mà mô hình đang xây dựng trên đó. Thay vì tốn tokens để van lọc mô hình nhớ một bất biến, chúng ta sắp xếp mã để bất biến đó khó bị vi phạm một cách ngẫu nhiên: lấy thuộc tính bạn quan tâm nhất, biểu diễn nó dưới dạng mà máy có thể kiểm tra, chiếu nó vào phần triển khai, và để vòng lặp nảy ra khỏi sự kiểm tra đó cho đến khi hiện vật mới thỏa mãn nó.

Shen-Backpressure: Áp lực ngược từ nền tảng

Shen-Backpressure là công cụ và phương pháp luận được xây dựng để khám phá giả thuyết này. Thay vì chờ đợi một mô hình thông minh hơn, công cụ này sử dụng Shen — một ngôn ngữ Lisp nhỏ, tĩnh kiểu với hệ thống kiểu sequent-calculus — để viết các quy tắc dưới dạng mà máy có thể chiếu vào nền tảng: các kiểu dữ liệu, hàm tạo và lệnh cổng (gate commands) trong ngôn ngữ đích mà mô hình phải viết dựa trên đó.

Bạn viết đặc tả một lần; một trình tạo mã (shengen) sẽ hạ cấp nó thành các kiểu bảo vệ (guard types) trong ngôn ngữ đích của bạn. Mô hình đang viết Go hay TypeScript không cần biết Shen tồn tại. Nó chỉ cần mã biên dịch được và các cổng kiểm tra phải vượt qua.

Chuỗi chứng minh cho ủy quyền đa khách hàng

Đây là phần cốt lõi của bản demo API đa khách hàng (multi-tenant API). Các quy tắc được viết trong Shen yêu cầu các điều kiện tiên quyết phải được thỏa mãn trước khi kết luận bên dưới đường kẻ ngang có thể được xây dựng.

Để có quyền truy cập tài nguyên (resource-access), bạn cần quyền truy cập khách hàng (tenant-access) và bằng chứng tài nguyên đó thuộc sở hữu của bạn. Để có tenant-access, bạn cần một chủ thể đã xác thực (authenticated principal) và bằng chứng là thành viên. Chuỗi đầy đủ chạy từ jwt-token -> authenticated-user -> tenant-access -> resource-access.

Các kiểu dữ liệu này đóng vai trò là nhân chứng. Việc xây dựng một giá trị thuộc một trong các kiểu này yêu cầu phải giải quyết các điều kiện tiên quyết được khai báo trong quy tắc của nó.

Từ đặc tả đến kiểu bảo vệ

shengen hạ cấp mỗi quy tắc thành một kiểu bảo vệ trong ngôn ngữ đích. Trong Go, các trường là không xuất khẩu (unexported), và hàm tạo được tạo ra là cách duy nhất để điền giá trị vào:

type TenantAccess struct {
    principal AuthenticatedPrincipal
    tenant    TenantId
    isMember  bool
}

func NewTenantAccess(principal AuthenticatedPrincipal, tenant TenantId, isMember bool) (TenantAccess, error) {
    if !(isMember == true) {
        return TenantAccess{}, fmt.Errorf("isMember must equal true")
    }
    return TenantAccess{principal: principal, tenant: tenant, isMember: isMember}, nil
}

Không có thủ thuật kỳ lạ nào ở đây, chỉ là khả năng hiển thị thông thường của Go. Mã bên ngoài gói không thể viết TenantAccess{isMember: true} vì các trường viết thường. Hàm tạo là con đường duy nhất đến một giá trị đã điền, và nó từ chối isMember == false.

ủy quyền mà không cần kiểm tra thủ công

Cách thông thường để viết một trình xử lý đa khách hàng là đặt một câu lệnh if vào mọi điểm cuối. Mô hình đó hợp lý, nhưng chính là loại điều hợp lý mà mọi người hay quên ở trình xử lý thứ bảy hoặc lần tái cấu trúc thứ ba.

Trong phiên bản Shen-Backpressure, việc kiểm tra thành viên vẫn tồn tại. Vẫn có truy vấn cơ sở dữ liệu, nhưng nó được tập trung tại ranh giới xây dựng cho TenantAccess thay vì rải rác khắp các trình xử lý như một quy ước.

Trình xử lý sau đó hoạt động trên một giá trị đại diện cho chuỗi đã được duyệt qua. Bằng chứng đi kèm với giá trị đó. Nếu tác nhân AI cố gắng bỏ qua chuỗi và chuyển một giá trị thô, quá trình xây dựng sẽ thất bại ngay lập tức.

Thông điệp ngắn gọn, máy móc "không" đó chính là áp lực ngược. Chúng ta cần nhiều thứ như vậy hơn, và ít đoạn văn trong prompt hơn.

Kết luận: Cần tín hiệu xác định hơn là mô hình thông minh hơn

Đối với các vòng lặp lập trình AI trong môi trường sản xuất, bạn cần áp lực ngược tốt hơn là cần một mô hình tốt hơn. Bạn cần các tín hiệu xác định (deterministic signals) cho biết hiện vật có hình dạng bạn mong muốn hay không. Kiểm thử cung cấp một tín hiệu như vậy, trình biên dịch cung cấp một tín hiệu khác, và một đặc tả Shen được hạ cấp thành các kiểu bảo vệ mở rộng bề mặt từ chối của trình biên dịch xa hơn nữa — các ràng buộc hình dạng chứng minh đi từ ý định thiết kế vào chính mã nguồn.

Không có điều nào trong số này là một cược chống lại các mô hình tốt hơn. Nhưng năng lực và sự chắc chắn là hai thứ khác nhau. "Mô hình này đáng tin cậy" là một tuyên bố về người viết; "hiện vật này duy trì bất biến" là một tuyên bố về một đối tượng cụ thể trước mặt bạn. Đó là lý do tại sao các đường đi sai trở nên khó thực hiện một cách ngẫu nhiên về mặt cấu trúc lại quan trọng ở mọi cấp độ năng lực của mô hình.