Skip to content

Power of 10 của NASA/JPL: 10 quy tắc viết mã C an toàn và vụ Toyota

Power of 10

Power of 10 là bộ 10 quy tắc viết mã C do Gerard Holzmann (NASA/JPL) công bố năm 2006, và từng được nhóm phần mềm của NASA dùng làm một thước đo khi đánh giá firmware bướm ga điện tử của Toyota. Bài viết giới thiệu bộ quy tắc, xét quy tắc nào áp dụng được nguyên văn và quy tắc nào cần điều chỉnh trong hệ thống nhúng Linux thời gian thực, rồi trình bày cách đưa chúng vào quy trình kiểm tra tự động.

Đánh giá firmware Toyota bằng Power of 10

Năm 2010, NASA Engineering and Safety Center (NESC) hỗ trợ Cục Quản lý An toàn Giao thông Đường cao tốc Hoa Kỳ (NHTSA) điều tra các báo cáo về hiện tượng tăng tốc ngoài ý muốn trên xe Toyota. Khi phân tích tĩnh mã nguồn hệ thống điều khiển bướm ga điện tử (ETCS-i) của Camry 2005, nhóm phần mềm của NASA kiểm tra cả mức tuân thủ Power of 10. Phụ lục A của báo cáo (Bảng A.8-5, trang 30) ghi nhận 9.603 cảnh báo, chia thành 9 nhóm và liên quan đến ít nhất 6 trong 10 quy tắc: biến có phạm vi rộng hơn cần thiết, tham số không được kiểm tra trước khi dùng, 200 hàm dài quá 75 dòng, 59 vòng lặp có thể không có cận trên, con trỏ ẩn trong typedef và macro có thể đệ quy. Đây là cảnh báo của công cụ, không phải tất cả đều là lỗi đã được xác nhận.

Vi phạm quy tắc không đồng nghĩa với lỗi gây tai nạn. Báo cáo công bố đầu năm 2011 kết luận NASA không tìm thấy lỗi điện tử nào đủ để mở bướm ga lớn và gây tăng tốc nguy hiểm, dù cũng không loại trừ khả năng phần mềm gây ra sự cố. Năm 2013, trong vụ kiện Bookout tại Oklahoma, bồi thẩm đoàn ra phán quyết bất lợi cho Toyota sau lời khai của Michael Barr về chất lượng mã nguồn ETCS.

The Power of 10 do Gerard Holzmann thuộc Laboratory for Reliable Software của NASA/JPL (Jet Propulsion Laboratory) công bố năm 2006. Bộ quy tắc chỉ gồm 10 điều, viết cho ngôn ngữ C, và đủ cụ thể để được dùng làm thước đo trong một cuộc điều tra độc lập.

Bài viết xét bộ quy tắc đó trong bối cảnh hệ thống nhúng Linux có yêu cầu xử lý thời gian thực: quy tắc nào áp dụng được nguyên văn, quy tắc nào cần điều chỉnh khi mã nguồn dùng DPDK (Data Plane Development Kit) và các cơ chế của kernel Linux. Nội dung là phân tích dựa trên đặc điểm kiến trúc phần mềm, không phải kết quả audit trên một codebase cụ thể.

Power of 10 và lý do chỉ có 10 quy tắc

Holzmann lập luận rằng hầu hết bộ coding guideline quá dài và quá mơ hồ, nên không ai nhớ và không công cụ nào kiểm tra được hết. Ông chọn cách ngược lại: giới hạn ở 10 quy tắc, mỗi quy tắc đủ cụ thể để máy kiểm tra được, đổi lại độ nghiêm ngặt cao.

Mục tiêu không phải làm code "đẹp". Mục tiêu là làm cho code dễ phân tích tĩnh, để công cụ có thể chứng minh những tính chất vượt xa việc tuân thủ quy tắc. Vì vậy, nhiều quy tắc thực chất nhằm giữ cho call graph (đồ thị lời gọi hàm) và luồng điều khiển đủ đơn giản để công cụ suy luận được.

Nội dung 10 quy tắc, diễn đạt lại:

  1. Luồng điều khiển đơn giản: không goto, setjmp/longjmp, không đệ quy.
  2. Mọi vòng lặp có cận trên mà công cụ chứng minh được.
  3. Không cấp phát bộ nhớ động sau giai đoạn khởi tạo.
  4. Mỗi hàm vừa một trang in, khoảng 60 dòng.
  5. Trung bình tối thiểu 2 assertion mỗi hàm.
  6. Khai báo dữ liệu với phạm vi nhỏ nhất có thể.
  7. Kiểm tra giá trị trả về của mọi hàm, và kiểm tra tham số đầu vào.
  8. Dùng preprocessor hạn chế.
  9. Chỉ một mức dereference con trỏ, không dùng function pointer.
  10. Biên dịch với mọi cảnh báo ở mức nghiêm nhất, chạy static analyzer mỗi ngày và đạt zero warning.

Bản gốc của Holzmann: paper PDF, đăng trên IEEE Computer, 39(6), 2006.

Quy tắc có thể áp dụng nguyên văn

Theo đánh giá của tác giả, bốn quy tắc dưới đây phù hợp trực tiếp với firmware nhúng và có thể áp dụng mà không cần điều chỉnh.

Quy tắc 4 và 8: hàm ngắn, hạn chế preprocessor. Hai quy tắc này thuộc về kỷ luật review hơn là kỹ thuật. Macro nhiều tầng khiến cả công cụ phân tích lẫn người đọc đều khó theo dõi luồng xử lý thực tế.

Quy tắc 7: kiểm tra giá trị trả về. Quy tắc yêu cầu mọi nơi gọi hàm kiểm tra giá trị trả về, và mọi hàm kiểm tra tham số đầu vào của chính nó. Khi cố ý bỏ qua kết quả, cần ép kiểu (void) để thể hiện đây là quyết định có chủ ý.

int ret = dev_set_config(dev_id, &cfg);
if (ret != DEV_OK) {
    log_err("dev_set_config failed dev=%u ret=%d", dev_id, ret);
    return ret;
}

Quy tắc 10: zero warning. Bật -Wall -Wextra từ ngày đầu của dự án dễ hơn nhiều so với việc xử lý một codebase đã tích lũy hàng nghìn cảnh báo. Theo đánh giá của tác giả, đây là quy tắc có chi phí áp dụng thấp so với lợi ích mang lại.

Quy tắc có thể cần điều chỉnh trước khi áp dụng

Hệ thống nhúng Linux xử lý thời gian thực thường có một số đặc điểm kiến trúc khiến việc áp dụng nguyên văn trở nên khó khăn: các core chuyên dụng chạy vòng lặp busy-poll (liên tục kiểm tra hàng đợi thay vì chờ ngắt), gói tin đi qua DPDK, và driver Linux được tổ chức quanh các bảng hàm (ops table). Với các quy tắc dưới đây, cách tiếp cận hợp lý là giữ mục tiêu của quy tắc và điều chỉnh cách thực hiện. Các phương án điều chỉnh là đề xuất của tác giả, không có trong bài gốc của Holzmann.

Quy tắc 1: không đệ quy, không goto

Cấm đệ quy phù hợp với stack kích thước nhỏ trong kernel và với yêu cầu thời gian thực. Ngược lại, goto cho dọn dẹp lỗi (goto err_free) là mẫu chuẩn trong code Linux, và thường giúp mã nguồn rõ ràng hơn so với các khối if lồng nhau. Cần ghi nhận trong tài liệu của dự án rằng dự án không áp dụng quy tắc gốc ở điểm này.

Quy tắc 2: mọi vòng lặp phải có cận trên

Core busy-poll nhận gói tin chạy một vòng lặp vô hạn theo thiết kế. Bài gốc cho phép ngoại lệ với vòng lặp không bao giờ kết thúc, với điều kiện công cụ chứng minh được vòng lặp đó không thể thoát. Phần cần giới hạn là các vòng lặp bên trong, ví dụ số gói tin xử lý trong mỗi lần poll:

#define RX_BURST 32

for (;;) {                       /* vòng chính: không bao giờ thoát */
    n = rx_burst(port, queue, pkts, RX_BURST);
    for (i = 0; i < n; i++) {    /* vòng trong: cận trên cố định */
        handle_pkt(pkts[i]);
    }
}

Quy tắc 3: không cấp phát động sau khởi tạo

Lý do của Holzmann là bộ cấp phát như malloc có hành vi không dự đoán được. DPDK rte_mempool phù hợp với mục tiêu này: toàn bộ buffer được cấp trước lúc khởi tạo, phần còn lại chỉ lấy và trả từ pool có kích thước cố định. Điều cần cấm là malloc/kmalloc trên hot path (đường xử lý gói tin, nơi độ trễ quyết định hiệu năng). Phương án đề xuất: cấp phát toàn bộ ở giai đoạn khởi tạo, hot path chỉ lấy buffer từ pool, và pool cạn phải là một lỗi có xử lý rõ ràng.

Quy tắc 5: mật độ assertion

Holzmann yêu cầu khi một assertion thất bại, chương trình phải thực hiện hành động phục hồi rõ ràng, ví dụ trả về mã lỗi cho hàm gọi. Vì vậy, với hệ thống cần vận hành liên tục, cách dùng BUG_ON kiểu kernel (dừng hệ thống khi điều kiện sai) không phải lựa chọn mặc định phù hợp.

if (!(start < end && end <= MAX_ENTRIES)) {
    return ERR_INVALID_RANGE;   /* assertion + recovery path */
}

Ngưỡng tối thiểu 2 assertion mỗi hàm khó áp dụng máy móc cho các hàm xử lý gói tin ngắn trên hot path. Phương án đề xuất: tập trung assertion tại ranh giới module và tại các điểm nhận dữ liệu từ bên ngoài.

Quy tắc 6: phạm vi dữ liệu nhỏ nhất

Biến toàn cục dùng để chia sẻ dữ liệu giữa các luồng hoặc core là nguồn phát sinh race condition phổ biến trong hệ thống đa nhân. Khai báo biến sát chỗ sử dụng giúp việc review race condition đơn giản hơn. Khi cần biến tồn tại suốt vòng đời chương trình, biến static trong phạm vi file vẫn tốt hơn biến toàn cục, dù chưa phải phạm vi nhỏ nhất theo đúng yêu cầu của quy tắc.

Quy tắc 9: một mức dereference, không function pointer

Đây là quy tắc khó tuân thủ nhất. Driver model của Linux, các ops table và việc DPDK gọi hàm rx/tx qua con trỏ hàm đều là function pointer. Cấm hoàn toàn là không khả thi trong thực tế. Cách thỏa hiệp hợp lý:

  • Chỉ cho phép function pointer trong ops table const, gán một lần lúc init.
  • Mỗi ops table có danh sách đầy đủ các hàm có thể được gọi, để call graph vẫn suy luận được.
  • Mỗi chỗ dùng phải có chú thích nêu lý do.

Với giới hạn một mức dereference, a->b->c là hai mức. Trong các stack giao thức, cấu trúc dữ liệu lồng nhau là phổ biến, nên quy tắc này dễ bị vi phạm trên diện rộng. Cách xử lý: lấy con trỏ con vào biến cục bộ rõ tên (port_cfg = ctx->port_cfg), vừa đúng quy tắc vừa dễ đọc hơn.

Ánh xạ 10 quy tắc vào công cụ kiểm tra chuyên nghiệp

Theo datasheet của Perforce, Klocwork 2024.2 kiểm tra được 7 trong 10 quy tắc cho C/C++. Bảng dưới ghép trạng thái đó với cách kiểm tra bổ sung cho từng quy tắc. Cột cuối là đề xuất của tác giả, không lấy từ datasheet.

Quy tắc Klocwork Kiểm tra bổ sung, ghi chú
1. Luồng điều khiển đơn giản Có Nếu dự án cho phép goto để dọn lỗi, đánh dấu ngoại lệ tại chỗ
2. Vòng lặp có cận trên Có Vòng busy-poll chính cần được ghi ngoại lệ có lý do
3. Không cấp phát động sau khởi tạo Có Giới hạn lời gọi cấp phát trong các hàm khởi tạo và hàm tạo pool
4. Hàm khoảng 60 dòng Không Script đo độ dài hàm trong CI, ví dụ lizard
5. Tối thiểu 2 assertion mỗi hàm Không Checklist code review; script chỉ đếm được số assertion, không đánh giá được chất lượng
6. Phạm vi dữ liệu nhỏ nhất Có Không cần bổ sung
7. Kiểm tra giá trị trả về và tham số Có Thêm __attribute__((warn_unused_result)) của GCC cho các API quan trọng
8. Hạn chế preprocessor Có Không cần bổ sung
9. Một mức dereference, không function pointer Có Ops table const được ghi ngoại lệ kèm chú thích
10. Zero warning, phân tích tĩnh hằng ngày Không -Wall -Wextra -Werror trong CI, chạy analyzer theo lịch hằng ngày

Đưa vào quy trình của dự án

Quy tắc không được kiểm tra tự động dễ trở thành khuyến nghị bị bỏ qua. Power of 10 đặt mục tiêu mọi quy tắc đều kiểm tra được bằng công cụ, vì vậy bước tiếp theo là đưa chúng vào CI (Continuous Integration, quy trình build và kiểm thử tự động mỗi khi mã nguồn thay đổi):

  1. Chặn merge trong CI khi compiler hoặc static analyzer phát sinh cảnh báo mới (quy tắc 10).
  2. Chạy analyzer có ánh xạ Power of 10 cho các quy tắc công cụ hỗ trợ, và bổ sung kiểm tra cho quy tắc 4, 5, 10 theo bảng ở mục trên.
  3. Ghi nhận ngoại lệ tại chỗ. Mỗi vi phạm có chủ ý cần một chú thích ngắn nêu lý do và một chỉ dẫn để công cụ bỏ qua đúng vị trí đó, không tắt kiểm tra cho cả file.

Kết luận

Giá trị của Power of 10 không nằm ở việc tuân thủ đủ 10 điều, mà ở việc buộc đội phát triển xác định rõ quy tắc nào áp dụng, quy tắc nào bỏ qua và lý do. Một bộ quy tắc ngắn, có ngoại lệ được ghi nhận rõ ràng, dễ duy trì và kiểm tra hơn một bộ coding convention dài nhưng ít được tham khảo.

Các quy ước chi tiết hơn được trình bày trong technote Coding Convention Overview. Bài viết này giải thích lý do và cách đọc; technote là tài liệu để tra cứu.

Tài liệu tham khảo

Số liệu về Toyota lấy từ Phụ lục A của báo cáo NESC; số liệu về Klocwork lấy từ datasheet của Perforce.