show/hide this revision's text 2 Added quote from Kunen

For more explanation about how to prove Con(ZFC)→Con(ZFC+¬CH) finitistically, I'd recommend Chapter VII, §9 of Kunen's book Set Theory: An Introduction to Independence Proofs. Here is one relevant paragraph:

We show that, given any finite list, $\phi_1, \ldots, \phi_n$, of axioms of, say, ZFC+¬CH, we can prove in ZFC that there is a countable transitive model for $\phi_1, \ldots, \phi_n$. The procedure involves finding (in the metatheory) another finite list $\psi_1, \ldots, \psi_m$ of axioms of ZFC, and proving in ZFC that given a countable transitive model $M$ for $\psi_1, \ldots, \psi_m$, there is a generic extension, $M[G]$, satisfying $\phi_1, \ldots, \phi_n$. The inelegant part of this argument is that the procedure for finding $\psi_1, \ldots, \psi_m$, although straightforward, completely effective, and finitistically valid, is also very tedious. We must list in $\psi_1, \ldots, \psi_m$ not only the axioms of ZFC "obviously" used in checking that $\phi_1, \ldots, \phi_n$ hold in $M[G]$ (e.g., if $\phi_1$ is the Power Set Axiom, then $\phi_1$ should be listed among $\psi_1, \ldots, \psi_m$), but also all the axioms needed to verify that various concepts are absolute for $M$ ("finite", "p.o.", etc.), as well as the axioms needed to show that certain mathematical results, such as the Δ-system lemma, hold in $M$.
show/hide this revision's text 1

You have almost answered your own question; it seems that the only part you are confused about is whether "the reflection principle operates outside ZFC."

One must, as always, distinguish between the formal system whose properties we are analyzing (in this case, ZFC), and the theory inside which we are making our arguments about said formal system. The latter is what we call the "meta-theory." When you ask if Con(ZFC)→Con(ZFC+¬CH) can be proved purely within ZFC, this can only mean: "Can the meta-theoretic argument itself be formalized in ZFC?" Note here that ZFC is playing two roles; it is the theory being studied, and also the (meta-)theory being used to prove things about ZFC. It's important to not to confuse these two roles.

Now, the reflection principle takes place "outside ZFC" only in the sense that it is being used in the meta-theoretic proof of Con(ZFC)→Con(ZFC+¬CH). But this doesn't mean that the meta-theoretical argument can't itself be formalized in ZFC; in fact, it can, and in fact it can be formalized in much weaker systems (I think primitive recursive arithmetic suffices).

For more explanation about how to prove Con(ZFC)→Con(ZFC+¬CH) finitistically, I'd recommend Chapter VII, §9 of Kunen's book Set Theory: An Introduction to Independence Proofs.