titleEliminating timing side-channel leaks using program repair

IEEE Computer Society

booktitle30th IEEE Symposium on Security and Privacy (S&P 2009), 17-20 May 2009, Oakland, California, USA
titlePractical Mitigations for Timing-Based Side-Channel Attacks on Modern x86 Processors

booktitleIEEE/ACM International Symposium on Code Generation and Optimization, CGO 2021, Seoul, South Korea, February 27 - March 3, 2021
titleMemory-Safe Elimination of Side Channels

USENIX Association

booktitleProceedings of the 14th USENIX Security Symposium, Baltimore, MD, USA, July 31 - August 5, 2005
titleShredding Your Garbage: Reducing Data Lifetime Through Secure Deallocation

booktitleProceedings of the 11st ACM SIGOPS European Workshop, Leuven, Belgium, September 19-22, 2004
titleData lifetime is a systems problem

booktitleInformation Systems Security - 7th International Conference, ICISS 2011, Kolkata, India, December 15-19, 2011, Procedings
seriesLecture Notes in Computer Science
titleA Semantic Hierarchy for Erasure Policies

IEEE Computer Society

booktitleIEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015
titleCryptographic Enforcement of Language-Based Information Erasure

booktitle6th International Workshop on Issues in the Theory of Security (WITS’06)
titleNon-Interference and Erasure Policies for Java Card Bytecode

booktitleProgramming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings
seriesLecture Notes in Computer Science
titleJust Forget It - The Semantics and Enforcement of Information Erasure

IEEE Computer Society

booktitleProceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008
titleEnd-to-End Enforcement of Erasure and Declassification

booktitleInformation Security Technology for Applications - 15th Nordic Conference on Secure IT Systems, NordSec 2010, Espoo, Finland, October 27-29, 2010, Revised Selected Papers
seriesLecture Notes in Computer Science
titleImplementing Erasure Policies Using Taint Analysis

IEEE Computer Society

booktitle32nd IEEE Symposium on Security and Privacy, S&P 2011, 22-25 May 2011, Berkeley, California, USA
titleVerification of Information Flow and Access Control Policies with Dependent Types

booktitleProceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007
titleValgrind: a framework for heavyweight dynamic binary instrumentation

journaltitleCommun. ACM
titleFormal verification of a realistic compiler

§ PROOFS

This section details the proofs of the theorems and lemmas introduced in <ref>.

* The proof of <ref> is given in

* The proof of <ref> is given in

* The proof of <ref>, which states the correctness of our
RelSE, is given in <Ref>,

* The proof of <ref>, which states that our RelSE is correct for
bounded-verification of constant-time, is given in <Ref>.

§.§ Proof of <ref>

<Ref> expresses that when the symbolic evaluation is stuck
on a state \(s_k\), there exist concrete configurations derived from \(s_k\)
which produce distinct leakages.

Because \(s_k\) is stuck, we know from <Ref> that an expression
\(\rel{\varphi}\) is leaked and that \(\secleak(\rel{\varphi}, \pc)\)
evaluates to false in the symbolic evaluation of \(s_k\). We also know that
there exists a model \(M\) such that
\(M \sat \pc \wedge \lproj{\rel{\varphi}} \neq \rproj{\rel{\varphi}}\).
Let \(c_k, c_k'\) be concrete configurations such that
\(c_{k} \concsym{l}{M} s_{k}\), and \(c_{k}' \concsym{r}{M} s_{k}\).
To show that the program is not constant-time at step \(k\), that is
\(c_k \cleval{\leakvar} c_{k+1}\) and \(c_k' \cleval{\leakvar'} c_{k+1}'\)
with \(\leakvar \neq \leakvar'\),
we proceed case by case on the symbolic evaluation, restricting to cases where
\(\secleak(\rel{\varphi}, \pc)\) might evaluate to false. There are two main

* Symbolic execution is stuck on the evaluation of an expression,

* Symbolic evaluation is stuck on the evaluation of an instruction.

SE stuck on an expression. First, we consider the case where the
symbolic execution is stuck on the evaluation of an expression, restricting to
the rule load as other cases cannot be stuck.

* Case load: In the symbolic execution, the
expression \(\load{\ e_{idx}}\) is evaluated with
\(\econf{\regmap,\smem,\pc}{e_{idx}} \eeval{} \rel{\iota}\) and
the index \(\rel{\iota}\) is leaked.
Assuming \(\secleak(\rel{\iota}, \pc)\) evaluates to false with the model
\(M\), then
\(M(\lproj{\rel{\iota}}) \neq M(\rproj{\rel{\iota}})\).
Moreover, because \(c_{k} \concsym{l}{M} s_{k}\) and
\(c_{k}' \concsym{r}{M} s_{k}\), we have from <ref>
\(c_{k}\ e_{idx} \ceeval{} M(\lproj{\rel{\iota}}) \text{ and } %
c_{k}'\ e_{idx} \ceeval{} M(\rproj{\rel{\iota}})\). Because
performing a step in the concrete execution leaks the value of
\(e_{idx}\), we have
\(c_k \cleval{\leakvar \cdot M(\lproj{\rel{\iota}})} c_{k+1}\) and
\(c_k' \cleval{\leakvar' \cdot M(\rproj{\rel{\iota}})} c_{k+1}'\)
with \({M(\lproj{\rel{\iota}}) \neq M(\rproj{\rel{\iota}})}\),
meaning that the execution is not constant-time at step \(k\).

SE stuck on an instruction. Second, we consider the case where the
symbolic evaluation is not stuck on the evaluation of an expression, but is
stuck on the evaluation of an instruction. This can happen when evaluating
rules store, ite and d_jump.

* Case store: In the symbolic execution, the
instruction \(\store{\ e_{idx}}{e_{val}}\) is evaluated with
\(\econf{\regmap,\smem,\pc}{e_{idx}} \eeval{} \rel{\iota}\) and
the index \(\rel{\iota}\) is leaked.
Similarly as in case load, we can show that we have
\(c_k \cleval{\leakvar \cdot M(\lproj{\rel{\iota}})} c_{k+1}\) and
\(c_k' \cleval{\leakvar' \cdot M(\rproj{\rel{\iota}})} c_{k+1}'\)
with \(M(\lproj{\rel{\iota}}) \neq M(\rproj{\rel{\iota}})\),
meaning that the execution is not constant-time at step \(k\).

* Case ite-true and ite-false: In
the symbolic execution, the instruction
\(ite~e~?~l_{true} : l_{false}\) is evaluated with
\(\econf{\regmap,\smem,\pc}{e} \eeval{} \rel{\varphi}\) and
\(\rlift{eq_0}\ \rel{\varphi}\) is leaked.
Assuming \(\secleak(\rlift{eq_0}\ \rel{\varphi}, \pc)\) evaluates
to false with the model \(M\), then
\({M(\lproj{\rel{\varphi}} = 0)} \neq M({\rproj{\rel{\varphi}} =
Moreover, because \(c_{k} \concsym{l}{M} s_{k}\) and
\(c_{k}' \concsym{r}{M} s_{k}\), we have from <ref>
\(c_{k}\ e \ceeval{} M(\lproj{\rel{\varphi}}) \text{ and } %
c_{k}'\ e \ceeval{} M(\rproj{\rel{\varphi}})\).
Therefore in one of the concrete executions, \(e\) evaluates to 0,
the rule ite-false is applied and the location
\(l_{false}\) is leaked; whereas in the other execution, \(e\) does
not evaluate to 0, the rule ite-true is applied and the
location \(l_{true}\) is leaked.
Finally, we have \(c_k \cleval{\leakvar \cdot l_{true}} c_{k+1}\)
and \(c_k' \cleval{\leakvar' \cdot l_{false}} c_{k+1}'\) (or
\(c_k \cleval{\leakvar \cdot l_{false}} c_{k+1}\) and
\(c_k' \cleval{\leakvar' \cdot l_{true}} c_{k+1}'\)), meaning
that the execution is not constant-time at step \(k\).

* Case d_jump: In the symbolic execution,
the instruction \(\mathtt{goto}\ e\) is evaluated with
\(\econf{\regmap,\smem,\pc}{e} \eeval{} \rel{\varphi}\). Let
\(M(\lproj{\rel{\varphi}}) = \mathtt{bv_l}\) and
\(M(\rproj{\rel{\varphi}}) = \mathtt{bv_r}\).
Assume \(\secleak(\rel{\varphi}, \pc)\) evaluates to false with the
model \(M\), then \(\mathtt{bv_l} \neq \mathtt{bv_r}\).
Moreover, because \(c_{k} \concsym{l}{M} s_{k}\) and
\(c_{k}' \concsym{r}{M} s_{k}\), we have from <ref>
that \(c_{k}\ e \ceeval{} \mathtt{bv_l} \text{ and } %
c_{k}'\ e \ceeval{} \mathtt{bv_r}\). In the concrete execution,
\(l_l \mydef \toloc(\mathtt{bv_l})\) and
\(l_r \mydef \toloc(\mathtt{bv_r})\) are leaked—note that
\(\toloc\) is defined for \(\mathtt{bv_l}\) and \(\mathtt{bv_r}\)
from <ref>. Because
\(\mathtt{bv_l} \neq \mathtt{bv_r}\) and \(\toloc\) is a
one-to-one correspondence, we have \(l_l \neq l_r\).
Therefore, we have \(c_k \cleval{\leakvar \cdot l_l} c_{k+1}\) and
\(c_k' \cleval{\leakvar' \cdot l_r} c_{k+1}'\) with
\(l_l \neq l_r\), meaning that the execution is not constant-time
at step \(k\).

§.§ Proof of <ref>

<ref> expresses that symbolic evaluation does not get stuck
up to \(k\), then for each pair of concrete executions following the same path
up to \(k\), there exists a corresponding symbolic execution.

(Induction on the number of steps k). Case
\(k = 0\) is trivial.

Let \(c_{k-1}\) and \(c_{k-1}'\) be concrete configurations and
\(s_{k-1}\) a symbolic configuration for which the inductive
hypothesis holds. We need to show that <ref>
still holds at step \(k\), meaning that for each concrete steps
\(c_{k-1} \cleval{\leakvar} c_{k}\) and
\(c_{k-1}' \cleval{\leakvar'} c_{k}'\), there exists a symbolic
configuration \(s_{k}\) and a model \(M'\) such that
\({c_{k} \concsym{l}{M'} s_{k}} ~\wedge~ {c_{k}' \concsym{r}{M'}
s_{k}}\) holds. This amounts to show that:

*  the location in \(s_k\) is the same as the
location in \(c_k\) and \(c_k'\),

*  there exists a model \(M_k\) such that
\(M_k \sat \pc_k\)

*  for all expressions \(e\), either symbolic
evaluation gets stuck, or
\(\econf{\regmap_{k}, \smem_{k}}{e} \eeval{} \rel{\varphi}\)
\(M_k(\proj{\rel{\varphi}}) = \mathtt{bv} \iff c_k'~e \ceeval{}
\mathtt{bv}\).

We can proceed case by case on the concrete evaluation of
\(c_{k-1}\) and \(c_{k-1}'\). Note that from <ref>,
\(c_{k-1}\) and \(c_{k-1}'\) are at the same program location and
therefore need to evaluate the same instruction.

Case store. Consider that an instruction
\(\store{\ e_{idx}}{e_{val}}\) is evaluated at step \(k-1\).
Let \(\rel{\iota}\) be the symbolic index and \(\rel{\nu}\) be the
symbolic value, meaning that
\(\econf{\regmap,\smem,\pc}{e_{idx}} \eeval{} \rel{\iota} \) and
\(\econf{\regmap,\smem,\pc}{e_{val}} \eeval{} \rel{\nu}\).
<ref> directly follows from the concrete and the symbolic
evaluation rules that both just increment the location by 1.
Next, we build the new model \(M_k\) as:

\begin{align*}
M_k \mydef M[\smem_k \mapsto \pair{m_l}{m_r}] \quad
\text{ where }& m_l \mydef M(\lproj{\smem})[M(\lproj{\rel{\iota}}) \mapsto M(\lproj{\rel{\nu}})]\\
\text{ and }&   m_r \mydef M(\rproj{\smem})[M(\rproj{\rel{\iota}}) \mapsto M(\rproj{\rel{\nu}})]
\end{align*}

Intuitively, \(M_k\) is equal to the old model \(M\) in which we add
the new symbolic memory \(\smem_k\), mapping to the concrete value
of the old memory \(M(\smem)\) where the index \(M(\rel{\iota})\)
maps to the value \(M(\rel{\nu})\). Notice that \(M_k \sat \pc_k\)
because \(M \sat \pc\) and we only added new definitions (thus not
changing satisfiability) from \(M\) and \(\pc\) to \(M_k\) and
\(\pc_k\). Thus <ref> holds.
Finally, we show <ref> by induction on the structure of
expressions: for any expression \(e\), if symbolic evaluation does
not get stuck then
\(M_k(\lproj{\rel{\varphi}}) = \mathtt{bv} \iff c_k~e \ceeval{}
\mathtt{bv}\) holds (case of the right projection is analogous).
Note that only the memory is updated from step \(k-1\) to step
\(k\), meaning that \(c_k\), \(s_k\), and \(M_k\) only differ from
\(c_{k-1}\), \(s_{k-1}\) and \(M\) on expressions involving the
memory. Thus, we only need to consider the rule load, as
the proof for other rules directly follows from
\(c_{k-1}\concsym{p}{M} s_{k-1}\), <ref>, and the
definition of \(M_k\).

Assume an expression \(\load{e}\) such that \(s_k\) does not get
stuck and let
\(\econf{\regmap_{k}, \smem_{k}}{e} \eeval{} \rel{\iota'}\) and
\(\econf{\regmap_{k}, \smem_{k}}{\load{e}} \eeval{} \rel{\nu'}\).
We show that if <ref> holds for the expression \(e\),
then it holds for the expression \(\load{e}\). Formally, we must
show that if
\({M_k(\lproj{\rel{\iota'}}) = \mathtt{bv_{idx}}} \iff {{c_k~{e}
\ceeval{} \mathtt{bv_{idx}}}}\)
\({M_k(\lproj{\rel{\nu'}}) = \mathtt{bv_{val}}} \iff {c_k~{\load{e}}
\ceeval{} \mathtt{bv_{val}}}\).

First, we can rewrite \(M_k(\lproj{\rel{\nu'}})\) as

\begin{align*}
&= M_k(select( \lproj{\smem_k},\lproj{\rel{\iota'}})) \text{ by symbolic rule
\rulename{load}}\\
&= M(\lproj{\smem})[M(\lproj{\rel{\iota}}) \mapsto M(\lproj{\rel{\nu}})][M_k (\lproj{\rel{\iota'}})] \text{ by def.\ of \(M_k\)}\\
\end{align*}

From this point, there are two cases, either [label=(*)]

* the address of the load is the same as the address of the
previous store,

* the address of the load is different from the address of the
previous store.

* The address of the load is the same as the address of the
previous store, i.e.,
\(M_k (\lproj{\rel{\iota'}}) = M(\lproj{\rel{\iota}})\).
Therefore we have \({M_k(\lproj{\rel{\nu'}}) = M(\lproj{\rel{\nu}})}\).
From the induction hypothesis, the concrete index of the load
evaluates to \(M_k(\lproj{\rel{\iota'}})\), that is
\({c_k~{e} \ceeval{} M_k( \lproj{\rel{\iota'}})}\) which can be
rewritten as \({c_k~{e} \ceeval{} M(\lproj{\rel{\iota}})}\).
From concrete rule store and
\(c_{k-1} \concsym{l}{M} s_{k-1}\), we know that the concrete
memory from \(c_{k-1}\) to \(c_k\) is updated at index
\(M(\lproj{\rel{\iota}})\) to map to the value
\(M(\lproj{\rel{\nu}})\). Thus, we have
\(c_k~\load{e} \ceeval{} M(\lproj{\rel{\nu}})\) and by rewriting,
\({c_k~{\load{e}} \ceeval{} M_k(\lproj{\rel{\nu'}})}\).  Therefore
we have shown that
\({M_k(\lproj{\rel{\nu'}}) = \mathtt{bv_{val}}} \iff {c_k~{\load{e}} \ceeval{} \mathtt{bv_{val}}}\).

* The address of the load is different from the address of
the previous store, i.e.,
\(M_k (\lproj{\rel{\iota'}}) \neq M(\lproj{\rel{\iota}})\). Therefore we have
\({M_k (\lproj{\rel{\nu'}}) = M(\lproj{\smem})[M_k (\lproj{\rel{\iota'}})]}\).
From the induction hypothesis, the concrete index of the load
evaluates to \(M_k(\lproj{\rel{\iota'}})\), that is
\(c_k~{e} \ceeval{} M_k(\lproj{\rel{\iota'}})\).
From concrete rule store, we know that the concrete
memory from \(c_{k-1}\) to \(c_k\) is only updated at address
\(M(\lproj{\rel{\iota}})\) and untouched at address
\(M_k(\lproj{\rel{\iota'}})\).
Plus, we know from \(c_{k-1} \concsym{l}{M} s_{k-1}\) that address
\(M_k(\lproj{\rel{\iota'}})\) maps to
\(M(\lproj{\smem})[M_k(\lproj{\rel{\iota'}})]\) in \(c_{k-1}\).
Therefore, in configuration \(c_k\), index
\(M_k(\lproj{\rel{\iota'}})\) maps to
\(M(\lproj{\smem})[M_k(\lproj{\rel{\iota'}})]\) which, by
rewriting, leads to
\({c_k~{\load{e}} \ceeval{} M_k(\lproj{\rel{\nu'}})}\).  Therefore
we have shown that
\({M_k(\lproj{\rel{\nu'}}) = \mathtt{bv_{val}}} \iff {c_k~{\load{e}} \ceeval{} \mathtt{bv_{val}}}\).

Case d_jump. Consider that an instruction
\(\mathtt{goto}\ e\) is evaluated at step \(k-1\).
Notice that \(e\) evaluates to the same value in \(c_{k-1}\) and
\(c_{k-1}'\) because both executions follow the same path, and let
\(\mathtt{bv}\) be this concrete value. Concrete rule
d_jump just sets the next location to
\(l_c = \toloc(\mathtt{bv})\).
Symbolic evaluation of rule d_jump, evaluates \(e\) to a
symbolic value \(\rel{\varphi}\), computes a model
\(M' \solver{} \pi \wedge \lproj{\rel{\varphi}} \wedge
\rproj{\rel{\varphi}}\) and sets the next location to
\(l_{s} = \toloc(M'(\lproj{\rel{\varphi}}))\).
Note that from <ref> and because symbolic execution does
not get stuck, the rule can be non-deterministically applied with
any model \(M'\) satisfying the constraint.

Therefore, we can apply the rule with \(M' = M\) which gives
\(l_{s} = \toloc(M(\lproj{\rel{\varphi}}))\).
Moreover, from the hypothesis \(c_{k-1} \concsym{p}{M} s_{k-1}\) and
<ref>, we have
\(M(\lproj{\rel{\varphi}}) = \mathtt{bv}\) so
\(l_{s} = \toloc(\mathtt{bv})\). Therefore we have shown how to make
a symbolic step such that \(l_{s_{k}} = l_{c_{k}}\) and
<Ref> holds.
Finally, <ref> directly follow from
\(c_{k-1} \concsym{p}{M} s_{k-1}\) and <ref> because
symbolic and concrete evaluation of expressions are not modified by
rule d_jump.

Other cases. Case s_jump is trivial
as only the location is updated to the same static value in both
concrete and symbolic evaluation.
Case assign is similar to case store
(and simpler because it only requires to reason about the value and
not the index).
Finally Cases ite_true and
ite_false are a bit similar to case
d_jump and rely on the fact that both concrete
executions follow the same path, therefore a symbolic rule (either
ite_true or ite_fale) can be applied to
match the execution of both \(c_k\) and \(c_k'\).

Conclusion. We have shown that we can perform a step in symbolic
execution from \(s_{k-1}\) to a state \(s_k\), and there exists a model \(M'\)
such that \(c_k \concsym{l}{M_k} s_k\) and \(c_k' \concsym{r}{M_k} s_k\).

§.§ Proof of <ref>

<Ref> claims the correctness of our symbolic execution, meaning
that for each symbolic execution and model \(M\) satisfying the path predicate,
the concretization of the symbolic execution with \(M\) corresponds to a valid
concrete execution.

(Induction on the number of steps k).  Case \(k = 0\) is trivial.

Consider symbolic configurations \(s_0\),
\(s_{k-1} \mydef \iconf{\locvar}{\regmap}{\smem}{\pc}\) for which
the induction hypothesis holds. That is, for each model \(M\) and
configurations \(c_0\), \(c_{k-1}\) such that
\(c_0 \concsym{p}{M} s_0\) and \(c_{k-1}\concsym{p}{M} s_{k-1}\), we
have \(c_0 \cleval{}^{k-1} c_{k-1}\).
Let \(s_k \mydef \iconf{\locvar_k}{\regmap_k}{\smem_k}{\pc_k}\)
be the symbolic state such that \(s_{k-1} \ieval{} s_{k}\).  We need
to show that for each model \(M_k\) and configurations \(c_0\) and
\(c_k\) such that \(c_0 \concsym{p}{M_k} s_0\) and
\(c_{k}\concsym{p}{M_k} s_{k}\), we have
\(c_{0} \cleval{}^{k} c_k\).

Build steps \(0\) to \(k-1\).
First, we build the concrete execution from steps \(0\) to \(k-1\). Because
\(M_k \sat \pc_k\) (from <ref>) and \(\pc\) is a sub-formula of
\(\pc_k\) (from symbolic evaluation), we have \(M_k \sat \pc\), thus we can
build \(c_{k-1}\) such that \(c_{k-1}\concsym{p}{M_k} s_{k-1}\). Similarly we
can build \(c_0\) such that \(c_0 \concsym{p}{M_k} s_0\). Finally, from the
induction hypothesis, we have \(c_0 \cleval{}^{k-1} c_{k-1}\).

Build step \(k-1\) to \(k\).
Second, we build the concrete execution from steps \(k-1\) to \(k\): we need
to show that there is a step from \(c_{k-1}\) to \(c_k\) where
\(c_k \concsym{p}{M_k} s_k\).
Because concrete semantics never gets stuck (<ref>) there
is a state \(c_k' \mydef \cconf{\locvar'}{\cregmap'}{\cmem'}\) such that
\(c_{k-1} \cleval{} c_{k}'\) and because the semantics is deterministic
(<ref>), this state is unique. Thus we need to show that
\(c_{k}' = c_{k}\), that is \(c_{k}' \concsym{p}{M_k} s_{k}\). Because
\(M_k \sat \pc_k\) (from \(c_{k}\concsym{p}{M_k} s_{k}\) and
<ref>), this amounts to show that:

*  the location in \(c_k'\) is the same as the location in \(s_k\),

*  for all expression \(e\), either symbolic
evaluation gets stuck, or
\(\econf{\regmap_{k}, \smem_{k}}{e} \eeval{} \rel{\varphi}\)
\(M_k(\proj{\rel{\varphi}}) = \mathtt{bv} \iff c_k'~e \ceeval{}
\mathtt{bv}\).

We can proceed case by case on the concrete evaluation of
\(c_{k-1}\). Note that from <ref>, \(c_{k-1}\) and
\(s_{k-1}\) are at the same program location and therefore both evaluate
the same instruction.

Case store. Consider that an instruction
\(\store{\ e_{idx}}{e_{val}}\) is evaluated at step \(k-1\).
Let \(\rel{\iota}\) be the symbolic index and \(\rel{\nu}\) be the
symbolic value, meaning that
\(\econf{\regmap,\smem,\pc}{e_{idx}} \eeval{} \rel{\iota} \) and
\(\econf{\regmap,\smem,\pc}{e_{val}} \eeval{} \rel{\nu}\).
<Ref> directly follows from the concrete and the symbolic
evaluation rules that both just increment the location by 1.
We prove <ref> by induction on the structure of
expressions: for any expression \(e\), if symbolic evaluation does
not get stuck then
\(M_k(\proj{\rel{\varphi}}) = \mathtt{bv} \iff c_k'~e \ceeval{}
\mathtt{bv}\) holds.
Note that only the memory is updated from step \(k-1\) to step
\(k\), meaning that \(c_k'\) and \(s_k\) only differ from
\(c_{k-1}\) and \(s_{k-1}\) on expressions involving the
memory. Thus, we only need to consider the rule load, as
the proof for other rules directly follows from
\(c_{k-1}\concsym{p}{M_k} s_{k-1}\) and <ref>.

Assume an expression \(\load{e}\) such that \(s_k\) does not get
stuck and let
\(\econf{\regmap_{k}, \smem_{k}}{e} \eeval{} \rel{\iota'}\) and
\(\econf{\regmap_{k}, \smem_{k}}{\load{e}} \eeval{} \rel{\nu'}\).
We show that if <ref> holds for the expression
\(e\), then it holds for the expression \(\load{e}\). Formally, we
must show that if
\({M_k(\proj{\rel{\iota'}}) = \mathtt{bv_{idx}}} \iff {{c_k'~{e}
\ceeval{} \mathtt{bv_{idx}}}}\)
\({M_k(\proj{\rel{\nu'}}) = \mathtt{bv_{val}}} \iff {c_k'~{\load{e}} \ceeval{} \mathtt{bv_{val}}}\).

First, we can rewrite \(M_k(\proj{\rel{\nu'}})\) as

\begin{align*}
&= M_k(select( \proj{\smem_k},\proj{\rel{\iota'}})) \text{ by symbolic rule
\rulename{load}}\\
&=  M_k(select(store(\proj{\smem_{k-1}}, \proj{\rel{\iota}}, \proj{\rel{\nu}}),\proj{\rel{\iota'}})) \text{ by symbolic rule
\rulename{store}}\\
\end{align*}

From this point, there are two cases, either [label=(*)]

* the address of the load is the same as the address of the
previous store,

* the address of the load is different from the address of the
previous store.

* The address of the load is the same as the address of the previous
store, i.e., \(M_k (\proj{\rel{\iota'}}) = M_k(\proj{\rel{\iota}})\).
Therefore, we have \({M_k(\proj{\rel{\nu'}}) = M_k(\proj{\rel{\nu}})}\).
From the induction hypothesis, the concrete index of the load
evaluates to \(M_k(\proj{\rel{\iota'}})\), that is
\({c_k'~{e} \ceeval{} M_k( \proj{\rel{\iota'}})}\) which can be
rewritten as \({c_k'~{e} \ceeval{} M_k(\proj{\rel{\iota}})}\).
From concrete rule store and , we know that the concrete
memory from \(c_{k-1}\) to \(c_k'\) is updated at index
\(M_k(\proj{\rel{\iota}})\) to map to the value
\(M_k(\proj{\rel{\nu}})\). Thus, we have
\(c_k'~\load{e} \ceeval{} M_k(\proj{\rel{\nu}})\) and by rewriting,
\({c_k'~{\load{e}} \ceeval{} M_k(\proj{\rel{\nu'}})}\).  Therefore
we have shown that:

\[{M_k(\proj{\rel{\nu'}}) = \mathtt{bv_{val}}} \iff {c_k'~{\load{e}} \ceeval{} \mathtt{bv_{val}}}\]

* The address of the load is different from the address of the previous
store, i.e.,
\(M_k (\proj{\rel{\iota'}}) \neq M_k(\proj{\rel{\iota}})\). Therefore:

\[{M_k(\proj{\rel{\nu'}})} = M_k(select(\proj{\smem_{k-1}},\proj{\rel{\iota'}})) = M_k(\proj{\smem_{k-1}})[M_k(\proj{\rel{\iota'}})]\]

From the induction hypothesis, the concrete index of the load
evaluates to \(M_k(\proj{\rel{\iota'}})\), that is
\(c_k'~{e} \ceeval{} M_k(\proj{\rel{\iota'}})\).
From concrete rule store, we know that the concrete
memory from \(c_{k-1}\) to \(c_k'\) is only updated at address
\(M_k(\proj{\rel{\iota}})\) and untouched at address
\(M_k(\proj{\rel{\iota'}})\).
Plus, we know from \(c_{k-1} \concsym{p}{M_k} s_{k-1}\) that address
\(M_k(\proj{\rel{\iota'}})\) maps to
\(M(\proj{\smem_{k-1}})[M_k(\proj{\rel{\iota'}})]\) in \(c_{k-1}\).
Therefore, in configuration \(c_k'\), address
\(M_k(\proj{\rel{\iota'}})\) also maps to
\(M(\proj{\smem_{k-1}})[M_k(\proj{\rel{\iota'}})]\) which, by
rewriting, leads to
\({c_k'~{\load{e}} \ceeval{} M_k(\proj{\rel{\nu'}})}\).  Therefore
we have shown that:

\[{M_k(\proj{\rel{\nu'}}) = \mathtt{bv_{val}}} \iff {c_k'~{\load{e}} \ceeval{} \mathtt{bv_{val}}}\]

Case d_jump. Consider that an instruction
\(\mathtt{goto}\ e\) is evaluated at step \(k-1\).
Let \(\rel{\varphi}\) be the symbolic value of \(e\), meaning that
\(\econf{\regmap,\smem,\pc}{e} \eeval{} \rel{\varphi}\).
Symbolic rule d_jump sets the location to
\(l_{s_{k}} = \toloc(M(\lproj{\rel{\varphi}}))\), which is equal to
\(\toloc(M(\rproj{\rel{\varphi}}))\) because \(M\) satisfies the
constraint \(\lproj{\rel{\varphi}} = \rproj{\rel{\varphi}}\).
Concrete rule d_jump evaluates expression \(e\) to a
concrete value \(\mathtt{bv}\) and sets the location to
\(l_{c_{k}} = \toloc(\mathtt{bv})\). From the hypothesis
\(c_{k-1} \concsym{p}{M_k} s_{k-1}\) and <ref> we have
\(\mathtt{bv} = M_k(\proj{\rel{\varphi}})\), therefore
\(l_{c_{k}} = l_{s_{k}}\).

Finally, <ref> directly follows from
\(c_{k-1} \concsym{p}{M_k} s_{k-1}\) and <ref> because
symbolic and concrete evaluation of expressions are not modified by
rule d_jump.

Other cases. Case s_jump is trivial as only
the location is updated to the same static value in both concrete and symbolic
Case assign is similar to case store (and
simpler because it only requires to reason about the value and not the
Finally Cases ite_true and ite_false are
similar to case d_jump.

Conclusion. We have shown that \(c_{k-1} \cleval{} c_k'\) with
\(s_k \concsym{p}{M_k} c_k'\). Because \(\concsym{p}{M_k}\) is a tight
relation, we have \(c_k' = c_k\) and thus \(c_{k-1} \cleval{} c_k\).
Therefore, for each model \(M_k\) and configuration \(c_0\) and \(c_k\)
such that \(c_0 \concsym{p}{M_k} s_0\) and
\(c_{k} \concsym{p}{M_k} s_{k}\), we have \(c_{0} \cleval{}^{k} c_k\).

§.§ Proof of <ref>

<Ref> claims that if symbolic execution does not get stuck due to a
satisfiable insecurity query, then the program is constant-time.

(Induction on the number of steps k). Case
\(k = 0\) is trivial.

Let $s_0$ be an initial symbolic configuration for which the
symbolic evaluation never gets stuck. Let us consider a model \(M_0\)
and concrete configurations \(\cconfvar_0 \concsym{l}{M_0} s_0\),
\(\cconfvar'_0 \concsym{r}{M_0} s_0\), for which the induction
hypothesis holds at step \(k-1\), meaning that for all
\(c_{k-1} \mydef \cconf{\locvar}{\cregmap}{\cmem}\) and
\(c_{k-1}' \mydef \cconf{\locvar'}{\cregmap'}{\cmem'}\) such that
$c_0 \cleval{\leakvar}^{k-1} c_{k-1}$, $c_0' \cleval{\leakvar'}^{k-1} c_{k-1}'$,
then \(\leakvar = \leakvar'\). We show that <ref> still
holds at step \(k\).

From <ref>, there exists a model \(M\) and a
symbolic configuration
\(s_{k-1} \mydef \iconf{\locvar_s}{\regmap}{\smem}{\pc}\) such

\begin{equation}
\label{eq:2}
s_0 \ieval{}^{k-1} s_{k-1} ~\wedge~ c_{k-1} \concsym{l}{M} s_{k-1} ~\wedge~ c_{k-1}' \concsym{r}{M} s_{k-1}
\end{equation}

We show by contradiction that the leakages \(\mathtt{bv}\)
and \(\mathtt{bv'}\) produced by
\(c_{k-1} \cleval{\mathtt{bv}} c_{k}\) and
\(c_{k-1}' \cleval{\mathtt{bv'}} c_{k}'\) are equal.
Note that from <ref> and <ref>, we have
\(l_s = l = l'\), therefore the same instruction and expressions are
evaluated in configurations \(c_{k-1}, c_{k-1}', \text{ and } s_{k-1}\).
Suppose that \(c_{k-1}\) and \(c_{k-1}'\) produce distinct
This can happen during the evaluation of rules load,
d_jump, ite_true, ite_false,

Case load. Concrete evaluation of an expression
\(\load{e}\) in configurations \(c_{k-1}\) and \(c_{k-1}'\) produces
leakages \(\mathtt{bv}\) and \(\mathtt{bv'}\) and, assuming the load
is insecure, we have \(\mathtt{bv} \neq \mathtt{bv'}\).
Symbolic evaluation evaluates the index to a symbolic expression
\(\rel{\iota}\) and ensures \(\secleak(\rel{\iota}, \pc)\) holds.
From <ref> and <ref>, we have \(M \sat \pc\),
\(\mathtt{bv} = M(\lproj{\rel{\iota}})\) and
\(\mathtt{bv'} = M(\rproj{\rel{\iota}})\).
Because we assumed \(\mathtt{bv} \neq \mathtt{bv'}\), then
\(M(\lproj{\rel{\iota}}) \neq M(\rproj{\rel{\iota}})\).  Therefore,
we have
\(M \sat \pc \wedge \lproj{\rel{\iota}} \neq \rproj{\rel{\iota}}\),
meaning that \(\secleak(\rel{\iota}, \pc)\) evaluates to false and
the symbolic execution is stuck, which is a contradiction.
Therefore \(\mathtt{bv} = \mathtt{bv'}\).

Cases d_jump, ite_true,
ite_false, store.  The reasoning is

We have shown that the hypothesis holds at step \(k\). If
$s_0 \ieval{}^{k} s_{k}$, then for all model \(M\) and initial configurations
\(\cconfvar_0 \concsym{l}{M} s_0 \) and \(\cconfvar'_0 \concsym{r}{M} s_0\)
such that
\(\cconfvar_0 \cleval{\leakvar}^{k-1} \cconfvar_{k-1} \cleval{\leakvar_k}
\cconfvar_{k}\)
\(\cconfvar_0' \cleval{\leakvar'}^{k-1} \cconfvar'_{k-1} \cleval{\leakvar_k'} \cconfvar'_{k}\)
where \(\leakvar = \leakvar'\),
then \(\leakvar \cdot \leakvar_k = \leakvar' \cdot \leakvar_k'\).

§ DEFINITION OF THE \(\LOOKUP\) FUNCTION FOR RELATIONAL INDEXES

This section re-defines the \(\lookup\) function, introduced in <ref>
for simple indexes, in order to consider relational indexes. Note that simple
indexes are enough as long as the leakage model that is considered subsumes the
memory obliviousness leakage model, and hence constraints memory indexes to be
equal in both executions—this is for instance the case for the constant-time
leakage model.

We recall that \(\compare(\iota,\kappa)\) is a comparison function based on
syntactic term equality, which returns true (resp. false) only if
\(\iota\) and \(\kappa\) are equal (resp. different) in any interpretation, and
is undefined (denoted \(\bot\)) if the terms are not comparable.

We first define an auxiliary function \(\slookup(\smemvar_n, \iota)\) that
checks if the (non-relational) index \(\iota\) matches the most recent
store operation in the (non-relational) memory \(\smemvar_n\). If it can
determine that the index of the store matches \(\iota\), it returns the
corresponding value; if it can determine that the index of the store is distinct
from \(\iota\), it is undefined; and if it cannot determine the (dis-)equality
of both indexes, or if \(\smemvar_{n}\) is the initial memory, it returns a
symbolic \(select\) operation from \(\smemvar_{n}\):

(_0, ι)    = select(_0, ι)

(_n, ι)    =

φ    if  _n = store(_n-1,κ,φ) ∧(ι,κ)

if  _n = store(_n-1,κ,φ) ∧(ι,κ)

select(_n, ι)     if _n = store(_n-1,κ,φ) ∧(ι,κ) =

We also define a deep lookup function \(\dlookup(\smemvar_n, \iota)\) that
returns the value corresponding to the index \(\iota\) in the memory
\(\smemvar_n\). Contrary to \(\slookup\), \(\dlookup\) recursively iterates
through the memory when it can determine that the index of a store is distinct
from \(\iota\) (i.e., when \(\slookup\) returns \(\bot\)). This function
corresponds to the standard read-over-write <cit.>

(_n, ι)    =

(_n, ι)     if  (_n, ι) ≠

(_n-1, ι)     if  (_n, ι) = ∧_n = store(_n-1,κ,φ)

Next, we define a function \(\dedup\) that deduplicates a pair of expression
\(\pair{\varphi_{l}}{\varphi_{r}}\) if it can syntactically determine the
equality of \(\varphi_{l}\) and \(\varphi_{r}\):

(φ_lφ_r)    =

φ_l     if  (φ_l,φ_r)

φ_lφ_r     otherwise

Finally, the function \(\lookup\) for relational indexes is defined as follows:

(_n, ι) = φ_p

∀p ∈{l,r}

(_n, ι) = (φ_lφ_r)

(_n, ι) =

∀p ∈{l,r}

(_n, ι) = (_n-1, ι)

(_n, ι) = φ_l

(_n, ι) =

(_n, ι)

(_n, ι) = (φ_lφ_r)

If both sides of the (relational) index \(\rel{\iota}\) match the most recent
store—or if the equality of the index with the most recent store cannot be
determined—then \(\lookup\) returns the corresponding deduplicated relational
expression (rule match). Notice than the match rule also
encompasses simple indexes as \(\proj{\simple{\iota}} = \iota\). In this case,
the \(\dedup\) function ensures that the returned value is simple.

If both sides of the current index \(\rel{\iota}\) are syntactically distinct
from the most recent store, then the store can be safely bypassed and \(lookup\)
is recursively called on the next store (rule miss). Notice that this
rule keeps the lookup for the right and left side synchronized.

Finally, if the index \(\rel{\iota}\) matches the most recent store on the left
side but not on the right side, the rule continues the lookup only on the right
side using \(\dlookup\) (rule match-l). A symmetric rule
match-r, applies when the index matches the most recent store on the
right side.

§ APPLICATION: VIOLATIONS INTRODUCED BY  IN A CONSTANT-TIME SORT FUNCTION

This section details vulnerabilities introduced by the  compiler
in a constant-time sort function, (partly) given in <ref>, where
in contains secret data. The LLVM code, given in
<ref>, contains two select operations at
line <ref> (resp.line <ref>), which conditionally select the lowest
(resp. greatest) element of in and store it to out[0]
(resp. out[1]). Notice that the source code and the LLVM code are
both constant-time: they do not contain secret-dependent control-flow and memory
accesses do not depend on secret data.

The compiled version of <ref> for the
architecture—which does not feature cmov instructions—is given
in <ref>. The select LLVM instructions of
<ref> are compiled to conditional jumps. Consequently, the
assembly code in <ref> contains two secret dependent jumps at
line <ref> and line <ref> and is
therefore insecure.

More interestingly, for the more recent architecture  featuring
cmov, the compiler introduces a secret dependent memory access. In
the assembly code for , given in <ref>,
edx is set at line <ref> to either the address
in+0 or in+4, depending on whether
in[0] <= in[1] (i.e., the result of the cmp instruction
at line <ref>). At line <ref>,
edx is then used as a load address. Consequently, the
address of the load depends on the outcome of the condition
in[0] <= in[1], which is secret, hence the assembly code in
<ref> is insecure.

These two vulnerabilities were automatically found by  during our study
on preservation of constant-time by compilers detailed in <ref>.
This example illustrates that reasoning about constant-time at source or LLVM
level in not sufficient.

§ SCALABILITY OF  ACCORDING TO INPUT DATA

In this section, we evaluate the scalability of  according to the size
of the input data.
We conduct this experiment on the subset of programs given in
<ref> that has variable input size. For these programs, we
report the median execution time for 5 runs of  for a base size
(\(S_1\)) and for multiples of base size, ranging from $S_{2} = 2 \times S_1$ to
$S_{6} = 6 \times S_1$. For stream ciphers, we set \(S_1\) to 500; for block
ciphers we, we set \(S_1\) to the size of a block; and for the remove padding
function we set \(S_1\) to 64 in order to get size values around 256, which is
the maximum padding size. Experiments were performed on a laptop with an AMD
Ryzen 7 PRO 3700U @ 2.30GHz processor and 14GB of RAM[Note that the
architecture used in this evaluation is different from the architecture used
in <ref>, hence results are not drectly comparable to
<ref>]. Results are reported in <ref>.
Additionally, <ref> shows the evolution of the execution time
according to the size.

Results. For most programs, the execution time is proportional to the size of
the input. Indeed for most programs, almost all queries are simplified and the
number of queries stays the same when increasing size of the input, meaning that
the variation of execution time is due to the symbolic execution engine (and not
to the solver). Consequently, the execution time is proportional to the number
of instruction explored, which is in turn proportional to the input size.

Three notable exceptions are ,
, and  for an
input size of \(S_5\). For , the execution time does not grow
linearly with the input size because the number (and complexity) of queries sent
to the solver increases with the size of the input. For
the execution time is dominated by a
large number of queries, which are independent from the input size. The
execution time slowly increases and reaches a plateau after a size of 256, which
is the maximum padding size—at this point increasing the size of the input
does not change the symbolic exploration. Finally, for
, the execution time seems to increase linearly but
drops for the size \(S_5\) (i.e., 2500). Manual investigation revealed that the
size 2500 results in a final loop iteration on a 4 bytes chunk, which triggers a
shortcut (introduced by the compiler) and results in less queries sent to the
solver (0 instead of 3).

To conclude, the scalability of  according to the input size mostly
depends on whether the number of queries depends on the input size. Fortunately,
in most of our cases, the number of queries does not vary with the input size
and the execution time of  scales linearly with the size of the input.


# Another Example of Nonparametric Generalized Ridge Regression

Robert L. Obenchain
Risk Benefit Statistics

(June 2023)

###### Abstract

The Two-Stage approach to optimal non-linear predictions via Generalized Ridge
Regression is again illustrated. This time, we use a model with six
$x-$predictors and more than $2,500$ observations. Unbiased estimates and
predictions are then compared with their corresponding “optimally biased”
estimates and predictions most likely to have minimal MSE risk under Normal
distribution theory. Again, we find that lower residual standard errors and
lower MSE risks relative to those lower errors predominate.

Keywords: Nonparametric Regression, Generalized Ridge Regression, Normal-
theory Maximum Likelihood, Mean-Squared-Error Risk, R-functions.

##  1 Introduction

We provide another example of the simple way to combine use of nonparametric
regression with optimally biased estimation of linear models introduced in
Obenchain (2023).

This new multiple regression strategy is applicable when $p\geq 2$ different
individual $x-$vectors are initially used alone (one-at-a-time) to make $p$
(different) nonparametric predictions of a single observed $y-$outcome vector.
When the number, $n$, of observations available is large ($n=2,793$ here),
using the gam() function from the mgcv $R-$package, Wood (2023), is strongly
recommended due to both its speed and efficiency.

TABLE 1 – Names and Descriptions of Variables
---
Var | Name | Description | Min | Max
y | AACRmort | Age Adjusted Circulatory-Respiratory Mortality | 95.5 | 46.00
x1 | Avoc | Anthropogenic Volatile Organic Compounds | 0.22282 | 2.8906
x2 | Bvoc | Biogenic Volatile Organic Compounds | 0.2611 | 3.3092
x3 | PREMdeath | Premature Death Index (before Age 75) | 2853 | 36469
x4 | ASmoke | Adult Smoking Percentage | 0.06735 | 0.41202
x5 | ChildPOV | Children Living in Poverty Index | 0.0290 | 0.6630
x6 | IncomIEQ | Income Inequality Index | 2.932 | 8.929

Our numerical example will use $p=6$ $x-$predictors of $y-$Outcome values of
“Age Adjusted Circulatory-Respiratory Mortality” rates for $2,793$ US Counties
in $2016$. A CSV file containing the data can be downloaded from Dryad, Young
and Obenchain (2022).

Upon completing this “Initial Phase” of analysis, the analyst forms an
$R-$data.frame containing the following $2*p+1$ variables: $(a)$ the observed
$y-$outcome vector, $(b)$ the $p$ $x-$predictor variables, and $(c)$ the $p$
$y-$predictor vectors, each of which is a nonparametric, non-linear function
of only one of the given $x-$predictor vectors.

Finally, the analyst uses the eff.ridge() and MLcalc() functions from the
“RXshrink” $R-$package, Obenchain (2022b), to first generate “TRACE” graphics
such as those displayed in Figure $3$ and then to calculate the relative $MSE$
risk statistics reported in Table $3$. Again, we find that the nonparametric
estimates with $MaximumLikelihood$ of being “optimally biased” under Normal
distribution-theory, Obenchain (2022a), generally tend to achieve both lower
“residual error” and lower “relative” MSE risk compared to unbiased (BLUE)
least squares estimates.

Figure 1:  These first four $gam()$ predictions of AACRmort rate $y-$outcomes
using, in turn, $x1=Avoc$, $x2=Bvoc$, $x3=PREMdeath$ and $x4=ASmoke$ are
clearly nonlinear and non-monotone. The $gam()$ predictions for $x1$ and $x3$
strike me as being particularly interesting. Figure 2:  These last two $gam()$
predictions of AACRmort rate $y-$outcomes using $x5=ChildPOV$ and
$x6=IncomIEQ$ are only slightly “curved”. While they strike me as less
interesting, they still provide “small” steps forward.

##  2 Linear Rank Deficiency

Regression models typically assume that (1) the n by p “centered” $X-$matrix,
$(I-11^{\prime}/n)X$, is of full (column) rank, $p$, and that (2) an
“intercept” term, $\mu$, is included to assure that the “fit” (a line, plane
or hyper-plane) passes through $y=\bar{y}$ in the $p+1$ dimensional Euclidean
space where all $x-$coordinates equal their mean vector. Specifically,

$\hat{\mu}=\bar{y}-\bar{x}^{\prime}\hat{\beta}\text{ .}$ (1)

Note that this intercept estimate automatically changes when the $\hat{\beta}$
coefficient vector is shrunken via generalized ridge regression, allowing the
implied “fit” to pivot about $\bar{x}$ in $p-$space.

##  3 Generalized Ridge Regression Shrinkage

Early proposals for choosing the “k-factor” defining the $1-$parameter
shrinkage path of Hoerl and Kennard (1970) were based mostly upon
“heuristics.” In sharp contrast, shrinkage based upon Normal-theory Maximum
Likelihood estimation has a firm theoretical foundation, Obenchain (1975,
1977, 1978). The Efficient $p-$parameter shrinkage-path is a two-piece linear
spline with a single interior Knot at the overall “best” (minimum MSE risk)
vector of point-estimates, Obenchain (2022a).

Ridge computations and TRACE displays for the Efficient Path (plus other
visualizations) are implemented in version $2.2$ of the RXshrink $R-$package,
Obenchain (2022b). Each TRACE typically displays estimates of $p\geq 2$
quantities that change as shrinkage occurs. The “coef” TRACE displays the $p$
fitted linear-model $\beta-$coefficients, while the “rmse” TRACE plots
relative mean-squared-error estimates given by the diagonal elements of the
MSE-matrix divided by the OLS-estimate of $\sigma^{2}$.

##  4 Overall Extent of Shrinkage

The multicollinearity allowance, $m$, measures the “extent” of shrinkage
applied.

$m=p-\delta_{1}-\cdots-\delta_{p}=rank(X)-trace(\Delta).$ (2)

Note that $0\leq m\leq p$, Obenchain (1977). Besides being the rank of $X$,
$p$ is also the $trace$ of the OLS Hat-matrix, $XX^{+}$. Similarly,
$trace(\Delta)$ is like a measure of “rank” for the diagonal ($p\times p$)
$\Delta$ shrinkage-factor matrix.

##  5 Correlations between Variables

Note that the $2,793$ observed $y-$Outcomes are correlated with the six given
$x-$variables and also are slightly more correlated with their six
$np-$prediction vectors, as shown in Table $2$.

TABLE 2 – Pearson Correlations between Two Sets of Seven Variables
---
variable | y |  | x1 | x2 | x3 | x4 | x5 | x6
y | 1.0000 |  |  |  |  |  |  |
x1 | 0.2489 |  | 1.00000 |  |  |  |  |
x2 | 0.4589 |  | 0.58472 | 1.0000 |  |  |  |
x3 | 0.6421 |  | 0.08896 | 0.4217 | 1.00000 |  |  |
x4 | 0.6047 |  | 0.32707 | 0.4622 | 0.67611 | 1.0000 |  |
x5 | 0.5524 |  | 0.11336 | 0.4884 | 0.69932 | 0.6605 | 1.0000 |
x6 | 0.3040 |  | 0.13933 | 0.4163 | 0.41804 | 0.3800 | 0.5708 | 1.0000
variable | y |  | np1 | np2 | np3 | np4 | np5 | np6
y | 1.0000 |  |  |  |  |  |  |
np1 | 0.3888 |  | 1.0000 |  |  |  |  |
np2 | 0.4809 |  | 0.5991 | 1.0000 |  |  |  |
np3 | 0.6769 |  | 0.3077 | 0.5117 | 1.0000 |  |  |
np4 | 0.6156 |  | 0.5002 | 0.5485 | 0.6621 | 1.0000 |  |
np5 | 0.5656 |  | 0.3029 | 0.5192 | 0.7348 | 0.6607 | 1.0000 |
np6 | 0.3379 |  | 0.1884 | 0.4378 | 0.4389 | 0.3775 | 0.5775 | 1.0000

##  6 Key Comparisons

Applied researchers should consider transforming the individual $x-$variables
available to them using nonparametric (polynomial spline) methods to improve
prediction of their target $y-$outcome variable. The one variable at a time
approach illustrated here provides a viable way to do this. Once a researcher
identifies $p=2$ or more predictor variables, two different sets of Maximum
Likelihood estimates under Normal distribution-theory (Unbiased or Optimally
Shrunken) should be computed and compared in several ways.

TABLE 3 – Key Statistical Comparisons for the Linear and NP Models
---
Linear Model Formula | $y\sim x1$ | $+x2$ | $+x3$ | $+x4$ | $+x5$ | $+x6$
Residual Mean Square | 0.506395 |  |  |  |  |
Residual Std. Error | 0.711615 |  |  |  |  |
OLS Beta Coefficients | 0.060975 | 0.136652 | 0.389470 | 0.216750 | 0.099290 | -0.063270
ML Optimally Biased Betas | 0.064848 | 0.134431 | 0.384555 | 0.218586 | 0.101132 | -0.062424
OLS Relative MSE Risks | 0.000613 | 0.000745 | 0.000821 | 0.000822 | 0.000968 | 0.000519
ML Minimum Relative Risks | 0.000292 | 0.000428 | 0.000756 | 0.000380 | 0.000524 | 0.000488
dMSE Estimates | 0.9996 | 0.9413 | 0.9964 | 0.9429 | 0.9728 | 0.003282
NP Model Formula | $y\sim np1$ | $+np2$ | $+np3$ | $+np4$ | $+np5$ | $+np6$
Residual Mean Square | 0.479143 |  |  |  |  |
Residual Std. Error | 0.692202 |  |  |  |  |
OLS Beta Coefficients | 0.098704 | 0.056765 | 0.451541 | 0.214582 | 0.035727 | -0.005387
ML Optimally Biased Betas | 0.103079 | 0.056651 | 0.443230 | 0.221146 | 0.034597 | -0.006164
OLS Relative MSE Risks | 0.000590 | 0.000715 | 0.000852 | 0.000815 | 0.000996 | 0.000533
ML Minimum Relative Risks | 0.000380 | 0.000559 | 0.000911 | 0.000790 | 0.000939 | 0.000453
dMSE Estimates | 0.9997 | 0.4332 | 0.9961 | 0.8721 | 0.9359 | 0.9882
Figure 3:  The two Traces of $\beta-$coefficients in the Top Row show that
relative magnitudes of effect estimates are initially unstable, with less
shrinkage (to $m=0.775$ rather than to $m=1.07$) being appropriate when the
six “non-linear” versions of the given $x-$variables are used in the model.
The corresponding pair of Relative Risk ($MSE/\sigma^{2}$) Traces in the
bottom row confirm that the six nonparametric (and non-linear) predictors of
mortality (AACRmort) rates provide better predictions. See Table 3 for more
detail on this finding. Figure 4:  This pairs() graphic depicts the “lower
panel” of scatter-plots for the $y-$Outcome ($AACRmort$) variable as well as
the $2$ pairs of most predictive $x$ and $np$ variables. The $x3$ and $np3$
variables quantify effects of the most important mortality predictor:
PREMdeath. Similarly, $x4$ and $np4$ quantify the relatively “well-known”
detrimental effects of ASmoke on mortality rates, having the second most-
positive ridge coefficients in Figure 3.

Note that Table $3$ (on page $8$) shows that the shrunken NP model achieves
not only lower residual error than the shrunken Linear model but also lower
MSE risks “relative to” that lower residual error for $5$ of the $6$ “np”
predictor variables!

Note that the optimally shrunken $x3=PREMdeath$ coefficient has an estimated
MSE risk of $0.5064*0.000756=0.000383$, while that of its $np3$ counterpart is
estimated to be larger: $0.4791*0.000911=0.000436$. All differences in MSE
risks and relative risks again tend to be small in this large scale EPA
Particulate Matter example, but achieving numerical risk reductions for $5$
out of $6$ relevant predictor variables certainly encourages use of the simple
“Two-Stage” approach illustrated here.

##  7 Summary

We have provided a second, much larger example ($p=6$ $x-$predictors and
$n=2,793$ observations) of the “two-stage” approach introduced in Obenchain
(2023). This is a straight-forward “common sense” way to non-linearly
transform predictor variables and, ultimately, generate “better” unbiased or
shrunken $y-$outcome predictions.

Computers have helped shape the theory as well as the practice of statistics
and data-science over the last 50 years. Software implementing accurate
computations and providing clear “visual insights” into the strengths and
weaknesses of alternative methods are indispensable components of an adequate
Tool Bag for today’s applied researchers.

##  8 References

Hastie, T. and Tibshirani, R. (1990). “Generalized Additive Models.” Chapman
and Hall.

Obenchain, R. L. (1975). “Ridge analysis following a preliminary test of the
shrunken hypothesis.” Technometrics 17, 431$-$441\.
http://doi.org/10.1080/00401706.1975.10489369

Obenchain, R. L. (1977). “Classical F-tests and confidence regions for ridge
regression.” Technometrics 19, 429$-$439\.
http://doi.org/10.1080/00401706.1977.10489582

Obenchain, R. L. (1978). “Good and Optimal Ridge Estimators.” Annals of
Statistics 6, 1111$-$1121\. http://doi.org/10.1214/aos/1176344314

Obenchain, R. L. (2022a). “Efficient Generalized Ridge Regression”, Open
Statistics 3, 1$–$18\. https://doi.org/10.1515/stat-2022-0108

Obenchain, R. L. (2022b). “RXshrink: Maximum Likelihood Shrinkage using
Generalized Ridge or Least Angle Regression Methods”, ver 2.2,
https://CRAN.R-project.org/package=RXshrink

Obenchain, R. L. and Young, S. S. (2023). “EPA Particulate Matter Data -
Analyses using Local Control Strategy.” North Carolina Journal of Mathematics
and Statistics 9, 1$–$24\. ISSN 2380-7539. Visit:
https://arxiv.org/abs/2209.05461

Wood, S.N. and Augustin, N.H. (2002), “GAMs with integrated model selection
using penalized regression splines and applications to environmental
modelling.” Ecological Modelling 157: 157$-$177\.

Wood, S.N., Pya N. and Saefken B. (2016), “Smoothing parameter and model
selection for general smooth models (with discussion). Journal of the American
Statistical Association 111: 1548$-$1575\.
http://doi:10.1080/01621459.2016.1180986

Wood, S.N. (2023), “mgcv: Mixed GAM Computation Vehicle with Automatic
Smoothness Estimation”, ver. 1.8-42, https://CRAN.R-project.org/package=mgcv

Young, S. S. and Obenchain, R. L. (2022). “EPA Particulate Matter Data”, Dryad
[Data Archive]. https://doi.org/10.5061/dryad.63xsj3v58