Is it possible to prove $Con(ZFC) \rightarrow Con(ZFC + \neg CH)$ purely within ZFC? To prove this (using forcing) one seems to need a countable transitive model of ZFC. The texts I am reading avoid this by proving Con(T + CH) for all (suitable) finite fragments T of ZFC using the Reflection principle to prove the existence of a countable transitive model of T. But doesn't the Reflection principle operate outside of ZFC? From what I understand it just shows how, given a list of axioms of ZFC, one can write down a proof that constructs a model of these axioms. Am I confused here or is there an other way to achieve this?

The reflection principle is a theorem scheme; each of its instances is provable in ZFC. The following proof works entirely in ZFC:
Btw, I think the sketch I just gave is not ideal since it seems to rely on the existence of infinite sets. The implication from Con(ZFC) to Con(ZFC+nonCH) can really be shown in ZF minus infinity, or even in a weak version of Peano arithmetic. 


The use of the Booleanvalued model approach to forcing allows one to avoid any consideration of countable transitive models in the proof that Con(ZFC) implies Con(ZFC+$\neg$CH), and gives in my opinion a more satisfying account of the result by dealing directly with models of full ZFC, rather than working with models only of some fragment of set theory. The point is that we have a very general procedure enabling us, starting from any model of ZFC, to produce a closely related model of ZFC+$\neg$CH. Specifically, suppose that $M$ is any model of ZFC. By the standard development of Booleanvalued models, as for example explained in Timothy Chow's A beginner's guide to forcing, or my notes on An introduction to the Boolean ultrapower, one may inside $M$ define the $\mathbb{B}$valued model $M^{\mathbb{B}}$, where $\mathbb{B}$ is the Boolean algebra in $M$ of the forcing $\text{Add}(\omega,\omega_2)^M$. These developments of forcing show that every axiom of ZFC gets Boolean value $1$ in $M^{\mathbb{B}}$, and further that $\\neg\text{CH}\=1$. Let $U$ be any ultrafilter on $\mathbb{B}$ in $M$, and form the quotient $M^{\mathbb{B}}/U$. The Los theorem for Boolean ultrapowers shows that this is a firstorder structure satisfying every statement whose Boolean value is in $U$. In particular, $M^{\mathbb{B}}/U$ satisfies ZFC+$\neg$CH. So we've shown that if there is a model of ZFC, then there is a model of ZFC+$\neg$CH, and this establishes the relative consistency result, as desired. The key to the success of the method is to develop the method of forcing internally in ZFC via the $\mathbb{B}$valued universe and its quotient. Thus, the construction of the model $M^{\mathbb{B}}$ and the quotient $M^{\mathbb{B}}/U$ is undertaken entirely inside the model $M$, as an internal ZFC construction. By this means, forcing becomes sensible over any model of ZFC. A careful consideration of the method shows that in fact the relative consistency result Con(ZFC)$\to$Con(ZFC+$\neg$CH) can be made in PA. One need only verify that PA can prove that ZFC proves the required development. But I prefer to leave this to the expertise of the proof theorists. 


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 "metatheory." When you ask if Con(ZFC)→Con(ZFC+¬CH) can be proved purely within ZFC, this can only mean: "Can the metatheoretic 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 metatheoretic proof of Con(ZFC)→Con(ZFC+¬CH). But this doesn't mean that the metatheoretical 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. Here is one relevant paragraph:



The usual strategy to prove that the negation of $CH$ is consistent with $ZFC$ is the following: One shows (under the assumption $Con(ZFC)$ that for any finite fragment $T$ of $ZFC$ we have that $T+ \lnot CH$ has a model. Here 'for any finite fragment' means that for each instance of such a finite $T$ one gets in a uniform way such a model. This is actually a scheme of theorems, one for each $T$. But this is still enough to obtain a proof for $Con (ZFC) \rightarrow Con(ZFC+ \lnot CH)$ inside $ZFC$: I will try it indirectly. Thus assume, to get a contradiction, that ''$ZFC \vdash CH$'' (this is an arithmetical statement using Gödel numbers, and should say in plain english: 'There exists a proof of $CH$ from $ZFC$'), then by Gödel we have: ''There exists a finite fragment $T$ of $ZFC$ such that $T \vdash CH$''(again this should read: 'There exists a proof...). We take this $T$ and apply our theorem scheme for $T$, i.e we actually prove in our uniform way that for our explicit theory $T+ \lnot CH$ has a model, which again by Gödel means that $T \nvdash CH$ which is a contradiction. This whole argument has taken place completely inside $ZFC$. 


The other answers are perfectly correct, but I'd like to add that the implication Con(ZFC) $\to $Con(ZFC + $\neg$CH) is not only provable in ZFC, it is provable in Peano arithmetic. I consider this a better and more natural version of the result  better since PA is much weaker than ZFC, so this version is more informative, and more natural because consistency is a number theoretic concept (no number $n$ is the Gödel number of a proof of 0=1). The reflection principle indeed operates outside of ZFC  it is a "theorem scheme" consisting of one theorem of ZFC for each sentence of set theory. However, the pattern of the proofs is quite simple, so that we can prove in PA a single theorem to the effect that each instance of reflection is a theorem of ZFC. A nice elementary way to treat forcing from the point of view of PA is to introduce a new system ZFC${}^+$ whose language is the language of ZFC augmented by a constant symbol $M$ and whose axioms consist of $\bullet$ the axioms of ZFC $\bullet$ the single assertion that $M$ is countable and transitive $\bullet$ the relativization of each axiom of ZFC to $M$. We then use reflection to prove, in PA, that if ZFC is consistent and we can construct in ZFC${}^+$ a set $N = M[G]$ in which both the axioms of ZFC and (say) $\neg$CH hold, then ZFC + $\neg$CH is consistent. I believe this technique is due to Shoenfield. (Shameless selfpromotion: this is the approach I use in my forthcoming book on forcing.) 

