Phương pháp xây dựng FSM từ netlist cấp cổng bằng công cụ REFSM, không sử dụng trừu tượng để đảm bảo không bỏ sót hành vi độc hại  

Các thuộc tính bảo mật được xây dựng từ giao thức bus AXI và các kịch bản tấn công Trojan phổ biến như rò rỉ thông tin và DoS  

Sử dụng UPPAAL để kiểm tra các thuộc tính bảo mật dưới dạng công thức trạng thái và công thức đường dẫn  

Thử nghiệm trên hệ thống SoC gồm 2 master, 3 slave và 1 module interconnect, với Trojan được cài vào 1 master và 1 slave  

Phát hiện Trojan rò rỉ thông tin bằng cách kiểm tra trạng thái nhận dữ liệu đồng thời của Slave B và Slave Trojan  

Phát hiện Trojan DoS bằng cách kiểm tra vòng lặp yêu cầu quyền truy cập bus liên tục từ Master Trojan  

Kết quả cho thấy các thuộc tính bảo mật được xây dựng có thể phát hiện chính xác nguồn gốc tấn công và loại bỏ false positive  

Phương pháp không yêu cầu sửa đổi phần cứng, không gây overhead về diện tích hay hiệu năng  

Đề xuất xây dựng thư viện thuộc tính bảo mật cho các giao thức bus khác nhau để mở rộng ứng dụng