AdaCore Enhances GCC Security with Innovative Features
by Fabien Chouteau –
In a significant stride towards bolstering the security of the open-source ecosystem, AdaCore has recently contributed a set of security hardening features to the GCC project (GNU Compiler Collection). These features, designed to fortify the software produced by GCC against various cyber threats, highlight our commitment to advancing the field of secure programming and our 30+ years of contributing to the open-source software development ecosystem.
Here is a quick overview of the features available in the next release of GCC (14):
Hardening Comparisons and Conditional Branches
To protect against control-flow attacks, the option -fharden-compares enables hardening of comparisons that compute results stored in variables, adding verification that the reversed comparison yields the opposite result.
For instance this comparison:
B := X = Y;Is expanded into:
B := X = Y;
declare
NotB : Boolean := X /= Y; -- Computed independently of B.
begin
if B = NotB then
<__builtin_trap>;
end if;
end;The option -fharden-conditional-branches enables hardening of comparisons that guard conditional branches, adding verification of the reversed comparison to both execution paths, turning:
if X = Y then
X := Z + 1;
else
Y := Z - 1;
end if;into:
if X = Y then
if X /= Y then -- Computed independently of X = Y.
<__builtin_trap>;
end if;
X := Z + 1;
else
if X /= Y then -- Computed independently of X = Y.
null;
else
<__builtin_trap>;
end if;
Y := Z - 1;
end if;It is difficult to predict which of these two options will affect a specific comparison operation expressed in source code. Using both options ensures that every comparison that is neither optimized out nor optimized into implied conditionals will be hardened.
Control Flow Redundancy Verification
The introduction of this new option prevents attacks that manipulate control flow within functions. With -fharden-control-flow-redundancy, the compiler now verifies, at the end of functions, whether the traversed basic blocks align with a legitimate execution path. The purpose of this protective measure is to detect and thwart attacks attempting to infiltrate the middle of functions, thereby enhancing the overall security posture of the compiled code.
Hardened Booleans for C and Ada
We have introduced a new type attribute, hardbool, for both the C and Ada programming languages. Hardened booleans allow users to define custom representations for true and false, each with a higher Hamming distance than standard booleans. These representations are rigorously validated at every use, effectively detecting memory corruption and certain malicious attacks.
Stack Scrubbing Control
A second type attribute, strub, enables stack scrubbing properties of functions and variables. Functions marked with strub trigger a zeroing-out of the stack frame upon return or exception escaping, fortifying against unauthorized access. Additionally, scalar variables tagged with this attribute implicitly enable stack scrubbing for any function containing or accessing them. This sophisticated feature enhances the protection against memory-based attacks, contributing to a more resilient software infrastructure.
Conclusion
By focusing on these critical elements, AdaCore enhances the resilience of GCC-compiled software against sophisticated adversarial techniques. Not only for Ada code, but also for C and other GCC supported languages (pending attribute implementation). Our dedication to advancing the security capabilities of GCC underscores the importance of proactive measures in the constantly evolving landscape of cyber threats. These new security hardening features provide developers with powerful tools to create more secure and robust software. As the industry continues to prioritize security, AdaCore's contributions to GCC mark a significant step towards a safer and more resilient software ecosystem.
About Fabien Chouteau
Fabien joined AdaCore in 2010 after his engineering degree at the EPITA (Paris). He is involved in real-time, embedded and hardware simulation technology. Maker/DIYer in his spare time, his projects include electronics, music and woodworking.