]>
Commit | Line | Data |
---|---|---|
a23e0209 AO |
1 | .. _Security_Hardening_Features: |
2 | ||
3 | *************************** | |
4 | Security Hardening Features | |
5 | *************************** | |
6 | ||
7 | This chapter describes Ada extensions aimed at security hardening that | |
8 | are provided by GNAT. | |
9 | ||
10 | .. Register Scrubbing: | |
11 | ||
12 | Register Scrubbing | |
13 | ================== | |
14 | ||
15 | GNAT can generate code to zero-out hardware registers before returning | |
16 | from a subprogram. | |
17 | ||
cf54619a | 18 | It can be enabled with the :switch:`-fzero-call-used-regs` command-line |
a23e0209 AO |
19 | option, to affect all subprograms in a compilation, and with a |
20 | :samp:`Machine_Attribute` pragma, to affect only specific subprograms. | |
21 | ||
22 | .. code-block:: ada | |
23 | ||
24 | procedure Foo; | |
25 | pragma Machine_Attribute (Foo, "zero_call_used_regs", "used"); | |
26 | -- Before returning, Foo scrubs only call-clobbered registers | |
27 | -- that it uses itself. | |
28 | ||
29 | function Bar return Integer; | |
30 | pragma Machine_Attribute (Bar, "zero_call_used_regs", "all"); | |
31 | -- Before returning, Bar scrubs all call-clobbered registers. | |
32 | ||
33 | ||
cf54619a | 34 | For usage and more details on the command-line option, and on the |
a23e0209 AO |
35 | ``zero_call_used_regs`` attribute, see :title:`Using the GNU Compiler |
36 | Collection (GCC)`. | |
37 | ||
38 | ||
39 | .. Stack Scrubbing: | |
40 | ||
41 | Stack Scrubbing | |
42 | =============== | |
43 | ||
44 | GNAT can generate code to zero-out stack frames used by subprograms. | |
45 | ||
46 | It can be activated with the :samp:`Machine_Attribute` pragma, on | |
47 | specific subprograms and variables. | |
48 | ||
49 | .. code-block:: ada | |
50 | ||
51 | function Foo returns Integer; | |
52 | pragma Machine_Attribute (Foo, "strub"); | |
53 | -- Foo and its callers are modified so as to scrub the stack | |
54 | -- space used by Foo after it returns. | |
55 | ||
56 | procedure Bar; | |
57 | pragma Machine_Attribute (Bar, "strub", "internal"); | |
58 | -- Bar is turned into a wrapper for its original body, | |
59 | -- and they scrub the stack used by the original body. | |
60 | ||
61 | Var : Integer; | |
62 | pragma Machine_Attribute (Var, "strub"); | |
63 | -- Reading from Var in a subprogram enables stack scrubbing | |
64 | -- of the stack space used by the subprogram. | |
65 | ||
66 | ||
cf54619a AO |
67 | There are also :switch:`-fstrub` command-line options to control |
68 | default settings. For usage and more details on the command-line | |
69 | option, and on the ``strub`` attribute, see :title:`Using the GNU | |
70 | Compiler Collection (GCC)`. | |
a23e0209 AO |
71 | |
72 | Note that Ada secondary stacks are not scrubbed. The restriction | |
73 | ``No_Secondary_Stack`` avoids their use, and thus their accidental | |
74 | preservation of data that should be scrubbed. | |
75 | ||
d235950e AO |
76 | Attributes ``Access`` and ``Unconstrained_Access`` of variables and |
77 | constants with ``strub`` enabled require types with ``strub`` enabled; | |
78 | there is no way to express an access-to-strub type otherwise. | |
79 | ``Unchecked_Access`` bypasses this constraint, but the resulting | |
80 | access type designates a non-strub type. | |
81 | ||
82 | .. code-block:: ada | |
83 | ||
84 | VI : Integer; | |
85 | XsVI : access Integer := VI'Access; -- Error. | |
86 | UXsVI : access Integer := VI'Unchecked_Access; -- OK, | |
87 | -- UXsVI.all does not enable strub in the enclosing subprogram. | |
88 | ||
89 | type Strub_Int is new Integer; | |
90 | pragma Machine_Attribute (Strub_Int, "strub"); | |
91 | VSI : Strub_Int; | |
92 | XsVSI : access Strub_Int := VSI'Access; -- OK. | |
93 | -- XsVSI.all enables strub in the enclosing subprogram. | |
94 | ||
95 | ||
96 | Every access-to-subprogram type, renaming, and overriding and | |
97 | overridden dispatching operations that may refer to a subprogram with | |
98 | an attribute-modified interface must be annotated with the same | |
99 | interface-modifying attribute. Access-to-subprogram types can be | |
100 | explicitly converted to different strub modes, as long as they are | |
101 | interface-compatible (i.e., adding or removing ``at-calls`` is not | |
102 | allowed). For example, a ``strub``-``disabled`` subprogram can be | |
103 | turned ``callable`` through such an explicit conversion: | |
104 | ||
105 | .. code-block:: ada | |
106 | ||
107 | type TBar is access procedure; | |
108 | ||
109 | type TBar_Callable is access procedure; | |
110 | pragma Machine_Attribute (TBar_Callable, "strub", "callable"); | |
111 | ||
112 | Bar_Callable_Ptr : constant TBar_Callable | |
113 | := TBar_Callable (TBar'(Bar'Access)); | |
114 | ||
115 | procedure Bar_Callable renames Bar_Callable_Ptr.all; | |
116 | pragma Machine_Attribute (Bar_Callable, "strub", "callable"); | |
117 | ||
118 | Note that the renaming declaration is expanded to a full subprogram | |
119 | body, it won't be just an alias. Only if it is inlined will it be as | |
120 | efficient as a call by dereferencing the access-to-subprogram constant | |
121 | Bar_Callable_Ptr. | |
95bb87b2 AO |
122 | |
123 | ||
124 | .. Hardened Conditionals: | |
125 | ||
126 | Hardened Conditionals | |
127 | ===================== | |
128 | ||
cf54619a | 129 | GNAT can harden conditionals to protect against control-flow attacks. |
95bb87b2 AO |
130 | |
131 | This is accomplished by two complementary transformations, each | |
132 | activated by a separate command-line option. | |
133 | ||
cf54619a AO |
134 | The option :switch:`-fharden-compares` enables hardening of compares |
135 | that compute results stored in variables, adding verification that the | |
95bb87b2 AO |
136 | reversed compare yields the opposite result. |
137 | ||
cf54619a AO |
138 | The option :switch:`-fharden-conditional-branches` enables hardening |
139 | of compares that guard conditional branches, adding verification of | |
140 | the reversed compare to both execution paths. | |
95bb87b2 AO |
141 | |
142 | These transformations are introduced late in the compilation pipeline, | |
143 | long after boolean expressions are decomposed into separate compares, | |
144 | each one turned into either a conditional branch or a compare whose | |
145 | result is stored in a boolean variable or temporary. Compiler | |
146 | optimizations, if enabled, may also turn conditional branches into | |
70c947e4 AO |
147 | stored compares, and vice-versa, or into operations with implied |
148 | conditionals (e.g. MIN and MAX). Conditionals may also be optimized | |
95bb87b2 AO |
149 | out entirely, if their value can be determined at compile time, and |
150 | occasionally multiple compares can be combined into one. | |
151 | ||
152 | It is thus difficult to predict which of these two options will affect | |
153 | a specific compare operation expressed in source code. Using both | |
70c947e4 AO |
154 | options ensures that every compare that is neither optimized out nor |
155 | optimized into implied conditionals will be hardened. | |
95bb87b2 AO |
156 | |
157 | The addition of reversed compares can be observed by enabling the dump | |
cf54619a AO |
158 | files of the corresponding passes, through command-line options |
159 | :switch:`-fdump-tree-hardcmp` and :switch:`-fdump-tree-hardcbr`, | |
160 | respectively. | |
95bb87b2 AO |
161 | |
162 | They are separate options, however, because of the significantly | |
163 | different performance impact of the hardening transformations. | |
d4fc83c6 AO |
164 | |
165 | ||
166 | .. Hardened Booleans: | |
167 | ||
168 | Hardened Booleans | |
169 | ================= | |
170 | ||
171 | Ada has built-in support for introducing boolean types with | |
172 | alternative representations, using representation clauses: | |
173 | ||
174 | .. code-block:: ada | |
175 | ||
176 | type HBool is new Boolean; | |
177 | for HBool use (16#5a#, 16#a5#); | |
178 | for HBool'Size use 8; | |
179 | ||
180 | When validity checking is enabled, the compiler will check that | |
181 | variables of such types hold values corresponding to the selected | |
182 | representations. | |
183 | ||
184 | There are multiple strategies for where to introduce validity checking | |
cf54619a AO |
185 | (see :switch:`-gnatV` options). Their goal is to guard against |
186 | various kinds of programming errors, and GNAT strives to omit checks | |
187 | when program logic rules out an invalid value, and optimizers may | |
188 | further remove checks found to be redundant. | |
d4fc83c6 AO |
189 | |
190 | For additional hardening, the ``hardbool`` :samp:`Machine_Attribute` | |
191 | pragma can be used to annotate boolean types with representation | |
192 | clauses, so that expressions of such types used as conditions are | |
cf54619a | 193 | checked even when compiling with :switch:`-gnatVT`. |
d4fc83c6 AO |
194 | |
195 | .. code-block:: ada | |
196 | ||
197 | pragma Machine_Attribute (HBool, "hardbool"); | |
198 | ||
cf54619a AO |
199 | Note that :switch:`-gnatVn` will disable even ``hardbool`` testing. |
200 | ||
201 | ||
202 | .. Control Flow Redundancy: | |
203 | ||
204 | Control Flow Redundancy | |
205 | ======================= | |
206 | ||
207 | GNAT can guard against unexpected execution flows, such as branching | |
208 | into the middle of subprograms, as in Return Oriented Programming | |
209 | exploits. | |
210 | ||
211 | In units compiled with :switch:`-fharden-control-flow-redundancy`, | |
212 | subprograms are instrumented so that, every time they are called, | |
213 | basic blocks take note as control flows through them, and, before | |
214 | returning, subprograms verify that the taken notes are consistent with | |
215 | the control-flow graph. | |
216 | ||
217 | Functions with too many basic blocks, or with multiple return points, | |
218 | call a run-time function to perform the verification. Other functions | |
219 | perform the verification inline before returning. | |
220 | ||
221 | Optimizing the inlined verification can be quite time consuming, so | |
222 | the default upper limit for the inline mode is set at 16 blocks. | |
223 | Command-line option :switch:`--param hardcfr-max-inline-blocks=` can | |
224 | override it. | |
225 | ||
226 | Even though typically sparse control-flow graphs exhibit run-time | |
227 | verification time nearly proportional to the block count of a | |
228 | subprogram, it may become very significant for generated subprograms | |
229 | with thousands of blocks. Command-line option | |
230 | :switch:`--param hardcfr-max-blocks=` can set an upper limit for | |
231 | instrumentation. | |
232 | ||
233 | For each block that is marked as visited, the mechanism checks that at | |
234 | least one of its predecessors, and at least one of its successors, are | |
235 | also marked as visited. Verification is normally performed just | |
236 | before return, but when a nonreturning call or a tail-call opportunity | |
237 | is detected, verification is moved before that (presumed) final call. | |
238 | ||
239 | If an exception from a nonreturning call is handled by its caller, | |
240 | verification at the caller may run again if another verification point | |
241 | is reached. The additional verifications are desirable and benign. | |
242 | ||
243 | Conversely, since no verification is inserted before calls that are | |
244 | expected to return, if they never do, the caller's own | |
245 | verification-and-return points are never reached. | |
246 | ||
247 | Subprogram executions that complete by raising or propagating an | |
248 | exception also bypass verification-and-return points. A subprogram | |
249 | that can only complete by raising or propagating an exception may have | |
250 | instrumentation disabled altogether. | |
251 | ||
252 | The instrumentation for hardening with control flow redundancy can be | |
253 | observed in dump files generated by the command-line option | |
254 | :switch:`-fdump-tree-hardcfr`. |