From ce0f6caae3c897ffd6c4d690cc38b23f4da238ce Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 25 Aug 2025 16:12:29 +0200 Subject: [PATCH 1/4] Test clightgen at most once --- tools/runner.sh | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/tools/runner.sh b/tools/runner.sh index f914c07d8..c2794fecc 100755 --- a/tools/runner.sh +++ b/tools/runner.sh @@ -173,6 +173,14 @@ Run_test() { make -C test SIMU="$1" test } +# Like Run_test, but don't test the clightgen tool, it's been done already + +Rerun_test() { + make -C test -s clean + make -C test CLIGHTGEN=false CCOMPOPTS="$2" -j$jobs all + make -C test CLIGHTGEN=false SIMU="$1" test +} + # Rounds of testing. # First parameter: round number (1, 2, ...) @@ -181,43 +189,43 @@ case "$target,$os" in aarch64,linux) case "$1" in 1) Run_test "$simu_aarch64" "";; - 2) Run_test "$simu_aarch64" "-fpic";; - 3) Run_test "$simu_aarch64" "-Os -fno-pie -no-pie";; + 2) Rerun_test "$simu_aarch64" "-fpic";; + 3) Rerun_test "$simu_aarch64" "-Os -fno-pie -no-pie";; esac;; aarch64,macos) case "$1" in 1) Run_test "" "";; - 2) Run_test "" "-fpic";; - 3) Run_test "" "-Os";; + 2) Rerun_test "" "-fpic";; + 3) Rerun_test "" "-Os";; esac;; arm,linux) case "$1" in 1) Run_test "$simu_armhf" "-marm";; - 2) Run_test "$simu_armhf" "-mthumb";; + 2) Rerun_test "$simu_armhf" "-mthumb";; 3) Rebuild_runtime -toolprefix arm-linux-gnueabi- arm-eabi - Run_test "$simu_armsf" "-marm";; + Rerun_test "$simu_armsf" "-marm";; esac;; ppc,linux) case "$1" in 1) Run_test "$simu_ppc32" "";; - 2) Run_test "$simu_ppc32" "-Os";; + 2) Rerun_test "$simu_ppc32" "-Os";; esac;; riscv,linux) case "$1" in 1) Run_test "$simu_rv64" "";; - 2) Run_test "$simu_rv64" "-fpic";; - 3) Run_test "$simu_rv64" "-Os -fno-pie -no-pie";; + 2) Rerun_test "$simu_rv64" "-fpic";; + 3) Rerun_test "$simu_rv64" "-Os -fno-pie -no-pie";; esac;; x86_32,*) case "$1" in 1) Run_test "" "";; - 2) Run_test "" "-Os";; + 2) Rerun_test "" "-Os";; esac;; x86_64,*) case "$1" in 1) Run_test "" "";; - 2) Run_test "" "-fpic";; - 3) Run_test "" "-Os -fno-pie -no-pie";; + 2) Rerun_test "" "-fpic";; + 3) Rerun_test "" "-Os -fno-pie -no-pie";; esac;; *) Fatal "Unknown configuration \"$target\" - \"$os\"" From 727a943b3b1271c98fc5a530e0903d4da634eef2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Jul 2025 13:56:01 +0200 Subject: [PATCH 2/4] x86-64: support IBT (control-flow integrity for indirect jumps) --- driver/Clflags.ml | 1 + driver/Driver.ml | 15 +++++++++++++-- runtime/x86_64/sysdeps.h | 14 ++++++++++++++ x86/TargetPrinter.ml | 24 ++++++++++++++++++++++-- 4 files changed, 50 insertions(+), 4 deletions(-) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 391e1ca1a..c5fa3434a 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -40,6 +40,7 @@ let option_mthumb = ref (Configuration.model = "armv7m") let option_Osize = ref false let option_finline = ref true let option_finline_functions_called_once = ref true +let option_fcf_protection = ref false let option_dprepro = ref false let option_dparse = ref false let option_dcmedium = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index 0052d3288..70a9e0ca1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -209,6 +209,8 @@ Code generation options: (use -fno- to turn off -f) -falign-branch-targets Set alignment (in bytes) of branch targets -falign-cond-branches Set alignment (in bytes) of conditional branches -fcommon Put uninitialized globals in the common section [on]. + -fcf-protection=branch Add control-flow integrity checks + -fcf-protection=none Don't add control-flow integrity checks |} ^ target_help ^ toolchain_help ^ @@ -278,6 +280,13 @@ let cmdline_actions = then option_fpie := true else warning no_loc Unnamed "option -fpie not supported on this platform, ignored" in + let set_cf_protection () = + match Configuration.arch, Configuration.model with + | "x86", "64" -> + option_fcf_protection := true + | _ -> + error no_loc "Option -fcf_protection=branch not supported on this target" + in [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; @@ -321,8 +330,10 @@ let cmdline_actions = Exact "-fpie", Unit set_pie_mode; Exact "-fPIE", Unit set_pie_mode; Exact "-fno-pie", Unset option_fpie; - Exact "-fno-PIE", Unset option_fpie ] @ - f_opt "common" option_fcommon @ + Exact "-fno-PIE", Unset option_fpie; + Exact "-fcf-protection=branch", Unit set_cf_protection; + Exact "-fcf-protection=none", Unset option_fcf_protection ] @ + f_opt "common" option_fcommon @ (* Target processor options *) (if Configuration.arch = "arm" then if Configuration.model = "armv6" then diff --git a/runtime/x86_64/sysdeps.h b/runtime/x86_64/sysdeps.h index a4e709575..884551e8a 100644 --- a/runtime/x86_64/sysdeps.h +++ b/runtime/x86_64/sysdeps.h @@ -38,6 +38,20 @@ .section .note.GNU-stack,"",%progbits +// The runtime library code is compatible with IBT and SHSTK + .section .note.gnu.property,"a" + .align 8 + .long 4 + .long 4f - 1f + .long 5 + .string "GNU" +1: .align 8 + .long 0xc0000002 + .long 3f - 2f +2: .long 0x3 +3: .align 8 +4: + #define GLOB(x) x #define FUNCTION(f) \ .text; \ diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 610be0f5a..7ff311a8a 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -183,7 +183,23 @@ module ELF_System : SYSTEM = let print_var_info = elf_print_var_info - let print_epilogue _ = () + let print_epilogue oc = + if !Clflags.option_fcf_protection then begin + output_string oc +{| .section .note.gnu.property,"a" + .align 8 + .long 4 + .long 4f - 1f + .long 5 + .string "GNU" +1: .align 8 + .long 0xc0000002 + .long 3f - 2f +2: .long 0x3 +3: .align 8 +4: +|} + end let print_comm_decl oc name sz al = fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al @@ -754,7 +770,9 @@ module Target(System: SYSTEM):TARGET = fprintf oc " leaq %a(%%rip), %a\n" label l ireg tmp1; fprintf oc " movslq (%a, %a, 4), %a\n" ireg tmp1 ireg r ireg tmp2; fprintf oc " addq %a, %a\n" ireg tmp2 ireg tmp1; - fprintf oc " jmp *%a\n" ireg tmp1 + fprintf oc " %sjmp *%a\n" + (if !Clflags.option_fcf_protection then "notrack " else "") + ireg tmp1 end else begin fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r end @@ -911,6 +929,8 @@ module Target(System: SYSTEM):TARGET = let print_instructions oc fn = current_function_sig := fn.fn_sig; + if !Clflags.option_fcf_protection then + fprintf oc " endbr64\n"; List.iter (print_instruction oc) fn.fn_code let print_optional_fun_info _ = () From b47870d86bdafe637bd2924c6c1bf0dd9d7af4c2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 19 Aug 2025 09:05:05 +0200 Subject: [PATCH 3/4] Use IBT by default on x86-64 BSD --- driver/Clflags.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index c5fa3434a..ec3fe894b 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -40,7 +40,10 @@ let option_mthumb = ref (Configuration.model = "armv7m") let option_Osize = ref false let option_finline = ref true let option_finline_functions_called_once = ref true -let option_fcf_protection = ref false +let option_fcf_protection = ref + (match Configuration.arch, Configuration.model, Configuration.system with + | "x86", "64", "bsd" -> true + | _ -> false) let option_dprepro = ref false let option_dparse = ref false let option_dcmedium = ref false From d3e528890ce9d70b06b4d7c56db119afe9cd707c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 19 Aug 2025 10:07:04 +0200 Subject: [PATCH 4/4] GHA CI: add test for -fcf-protection=branch on x86-64 --- .github/workflows/build.yml | 4 ++++ tools/runner.sh | 2 ++ 2 files changed, 6 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 4ef34fe69..0314ecbc5 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -42,6 +42,8 @@ jobs: run: tools/runner.sh test2 - name: Test alternate configuration 2 run: tools/runner.sh test3 + - name: Test alternate configuration 3 + run: tools/runner.sh test4 macos: runs-on: macos-latest env: @@ -68,3 +70,5 @@ jobs: run: tools/runner.sh test2 - name: Test alternate configuration 2 run: tools/runner.sh test3 + - name: Test alternate configuration 3 + run: tools/runner.sh test4 diff --git a/tools/runner.sh b/tools/runner.sh index c2794fecc..7cd1903d4 100755 --- a/tools/runner.sh +++ b/tools/runner.sh @@ -226,6 +226,7 @@ case "$target,$os" in 1) Run_test "" "";; 2) Rerun_test "" "-fpic";; 3) Rerun_test "" "-Os -fno-pie -no-pie";; + 4) Rerun_test "" "-fcf-protection=branch";; esac;; *) Fatal "Unknown configuration \"$target\" - \"$os\"" @@ -246,6 +247,7 @@ case "$1" in test1) Run_test_round 1;; test2) Run_test_round 2;; test3) Run_test_round 3;; + test4) Run_test_round 4;; build_ccomp) Build_ccomp;; check_proof) Check_proof;; hygiene) Hygiene;;