Morse-Kelley set theory consistency strength
This is an instance of a much more general result. (See Visser [2] for an overview of various related principles.) A theory is called sequential if it supports encoding of sequences of its objects with some basic properties. As a part of the definition (which I omit here as it is technical and not particularly relevant, it can be found in Pudlák [1]; see Visser [3] for more discussion), a sequential theory has some designated natural numbers (which serve as lengths of sequences) defined by a predicate $N(x)$. Usual theories of sets or classes are sequential, with $N(x)$ being $x\in\omega$.
Theorem: For any sequential theory $T$, the following are equivalent:
$T$ proves full induction: the schema $$\forall\bar y\,[\varphi(0,\bar y)\land\forall x\,(N(x)\land\varphi(x,\bar y)\to\varphi(x+1,\bar y))\to\forall x\,(N(x)\to\varphi(x,\bar y))]$$ for all formulas $\varphi$.
$T$ is uniformly essentially reflexive: for every formula $\varphi(x)$ and a finite subtheory $S\subseteq T$, $T$ proves $N(x)\land\Pr_S(\left\ulcorner\varphi(\dot x)\right\urcorner)\to\varphi(x)$, where $\Pr_S$ denotes the provability predicate for $S$, and $\dot x$ the numeral for $x$.
MK proves full induction, since it has induction for subsets of $\omega$, and the full comprehension schema guarantees that any property of natural numbers defined by a formula actually defines a subset of $\omega$. (Notice that this fails for NBG: due to the restrictions on its comprehension schema, NBG in general cannot prove induction for formulas with class quantifiers.) Thus, MK is uniformly essentially reflexive. In particular, if we take $0\ne0$ (with no occurrence of $x$) for $\varphi$, we see that MK proves $\neg\Pr_S(\left\ulcorner0\ne0\right\urcorner)$, i.e., $\mathrm{Con}_S$, for every its finite subtheory $S$, such as $S=\mathrm{NBG}$.
The main idea of the proof of $1\to2$ (which goes back to Montague) is that using sequence encoding, one can give partial truth definitions (i.e., truth definitions for any finite set of formulas including their substitution instances). Reasoning within the theory, if $S$ proves $\varphi$, then by the cut-elimination theorem, it has a sequent proof where each formula is a subformula of something in $S$ or $\varphi$. Using a partial truth definition for this finite set of formulas, one proves by induction on the length of proof that all sequents in the proof are true, hence also $\varphi$ holds.
References:
[1] Pavel Pudlák: Cuts, consistency statements and interpretations, Journal of Symbolic Logic 50 (1985), no. 2, pp. 423–441, doi: 10.2307/2274231.
[2] Albert Visser: An overview of interpretability logic, Logic Group Preprint Series vol. 174.
[3] Albert Visser: Pairs, sets and sequences in first order theories, Logic Group Preprint Series vol. 251.
Let me give an easier (sketch of an) answer to the part of the question about proving Con(ZFC) in MK. Unlike Emil's answer, the following does not cover the case of arbitrary finitely axiomatized subtheories of MK. Intuitively, there's an "obvious" argument for the consistency of ZFC: All its axioms are true when the variables are interpreted as ranging over arbitrary sets. (The universe is a model of ZFC, except that it isn't a set.) And anything deducible from true axioms is true, so you can't deduce contradictions from ZFC. The trouble with this argument is that it relies on a notion of "truth in the universe" that can't be defined in ZFC. What goes wrong if you try to define, in the language of ZFC, this notion of truth (or satisfaction) in the universe? Just as in the definition of truth in a (set-sized) model, you'd proceed by induction on formulas, and there's no problem with atomic formulas and propositional connectives. Quantifiers, though, give the following problem: The truth value of $\exists x\ \phi(x)$ depends on the truth values of all the instances $\phi(a)$, and there are a proper class of these. In showing that definitions by recursion actually define functions, one has to reformulate the recursion in terms of partial functions that give enough evidence for particular values of the function being defined. (For example, the usual definition of the factorial can be made into an explicit definition by saying $n!=z$ iff there is a sequence $s$ of length $n$ with $s_1=1$ and $s_k=ks_{k-1}$ for $2\leq k\leq n$ and $s_n=z$.) If you use the same method to make the definition of "truth in the universe" explicit, you find that the "evidence" (analogous to $s$ for the factorial) needs to be a proper class. So ZFC can't handle that (and it's a good thing it can't, because otherwise it would prove its own consistency). But MK can; it's designed to deal nicely with quantification of proper classes. So in MK, one can define what it means for a formula to be true in the ZFC universe. Then one can prove that all the ZFC axioms are true in this sense and truth is preserved by logical deduction (here one uses induction over the number of steps in the deduction). Therefore deduction from ZFC axioms can never lead to contradictions.
Concerning the fact that Kelley-Morse set theory proves Con(ZFC) and much more, I wrote a post on my blog explaining one way to do it.
Kelley-Morse implies Con(ZFC) and much more
The basic outline of the proof is to show that KM proves the existence of a class truth predicate Tr for first-order truth (and this is what Andreas also suggests in his answer), and then to prove that this truth predicate decrees that each axiom of ZFC is true. It follows by reflection that there will be rank initial segments $V_\theta$ that has the same satisfaction relation, and so these are transitive models of ZFC, and indeed KM proves that the universe is the union of a closed unbounded elementary tower $$V_{\theta_0}\prec V_{\theta_1}\prec\cdots\prec V_\lambda\prec\cdots\prec V.$$ Alternatively, a more syntactic argument proceeds by observing that the truth predicate is closed under deduction, complete and contains no explicit contradictions, and so it provides a complete consistent extension of ZFC.
Follow the link for the details.