Decidability of a first-order theory of hyperreals
Yes, the theory is decidable.
If $F$ is an ordered field and $R\subseteq F$ a non-cofinal subfield, then $$O=\{x\in F:\exists u\in R\:(-u\le x\le u)\}$$ is a convex valuation ring of $F$, with maximal ideal $$I=\{x\in F:\forall u\in R_{>0}\:(-u\le x\le u)\}.$$ $R$ embeds as a cofinal subfield in the residue field $O/I$; in general, the embedding may be proper, but if $R=\mathbb R$, then $R=O/I$, as $\mathbb R$ is complete.
Thus, let $T$ be the theory of structures $(F,R,+,\cdot,<)$ such that
$F$ is a real-closed field,
$R$ is a non-cofinal subfield of $F$, and
the canonical embedding of $R$ into the residue field $O/I$ as defined above is surjective (and therefore an isomorphism).
Then $T$ is a recursively axiomatized theory, it is valid in the hyperreal structures $({}^*\mathbb R,\mathbb R)$, and it is complete (see below), hence it is decidable, and axiomatizes the first-order theory of $({}^*\mathbb R,\mathbb R)$.
As pointed out in a comment by Erik Walsberg (thanks!), the completeness of $T$ is a special case of a more general result on tame elementary extensions of o-minimal structures due to Van den Dries and Lewenberg [1]. (Here, tameness is basically the axiom 3 above.) Their results also show that $T$ is model-complete, and in fact, that it has quantifier elimination in a language expanded with function symbols for roots of polynomials (which make the theory of real-closed fields universally axiomatized) and for the “standard part” map $\mathrm{st}\colon O\to R$ such that $x-\mathrm{st}(x)\in I$.
Let me indicate how to prove a weaker result: the theory $T_0$ of structures $(F,O)$ such that
$F$ is a real-closed field,
$O$ is a proper convex subring of $F$,
is complete and decidable. This follows from the Ax–Kochen–Ershov principle, which states that two henselian valued fields of residue characteristic $0$ with elementarily equivalent residue fields and value groups are elementarily equivalent.
First, it is an easy consequence of basic facts about valued fields that if $F$ is a real-closed field with a convex valuation ring $O$, then the valued field $(F,O)$ is henselian, the residue field $O/I$ is real-closed, and the value group $F^\times/O^\times$ is divisible.
Thus, if $(F,O)$ and $(F',O')$ are two models of $T_0$, their residue fields are elementarily equivalent by completeness of the theory of real-closed fields, and their value groups are elementarily equivalent by completeness of the theory of divisible totally ordered abelian groups, hence the valued fields $(F,O)$ and $(F',O')$ are elementarily equivalent by the AKE principle.
As shown by Cherlin and Dickman [2], $T_0$ has quantifier elimination in the language of ordered rings expanded with the predicate $$x\mid y\iff y\in xO.$$
References:
[1] Lou van den Dries, Adam H. Lewenberg: $T$-convexity and tame extensions, Journal of Symbolic Logic 60 (1995), no. 1, pp. 74–102, doi: 10.2307/2275510. On JSTOR.
[2] Gregory Cherlin, Max A. Dickmann: Real closed rings II. Model theory, Annals of Pure and Applied Logic 25 (1983), no. 3, pp. 213–231, doi: 10.1016/0168-0072(83)90019-2.