Is there a characterization of the topos of finite sets in the internal language? The topos ${\mathcal{Set}}$, at least as axiomatized in ETCS, is a well-pointed topos that satisfies the axiom of choice and has a natural numbers object. 
Is there a characterization of the topos ${\mathcal{FinSet}}$ in the internal language?  
 A: Characterization is too strong; there are many models of $\operatorname{ETCS}$, so its axioms don't characterize $\operatorname{Set}$ either.  But I'll interpret your question as asking how the axioms of $\operatorname{ETCS}$ might be changed if the intended model is $\operatorname{Fin}\operatorname{Set}$ instead of $\operatorname{Set}$.
Of course, you must remove the existence of the natural numbers object, and that might be sufficient; I mean, if you just want to have a topos whose internal mathematics is finitist in the weak sense that it doesn't assume the existence of any completed infinity, then this is sufficient.  Both $\operatorname{Fin}\operatorname{Set}$ and $\operatorname{Set}$ are models of this theory.
If you want to more assertively claim that the objects should be finite sets, then a strong way to do this is to add the following axiom scheme, where $\Phi$ is any property (in the language of $\operatorname{ETCS}$) of sets (objects):
$$ \Phi(0) \;\Rightarrow\; (\forall\,S\colon \operatorname{Ob},\; \Phi(S) \;\Rightarrow\; \Phi(S + 1)) \;\Rightarrow\; \forall\,S\colon \operatorname{Ob},\; \Phi(S) \text.$$
(Here I've chosen a particular way of phrasing the language of $\operatorname{ETCS}$ that hopefully makes sense to you.)
We can make this a finite axiomatization by requiring finiteness set by set:
$$ \forall\,X\colon \operatorname{Ob},\; \forall\,\mathcal{C}\colon \mathcal{P}\mathcal{P}X,\; \emptyset_X \in_{\mathcal{P}X} \mathcal{C} \;\Rightarrow\; (\forall\,S\colon \mathcal{P}S,\; \forall\,a\colon X,\; \neg\,(a \in_X S) \;\Rightarrow\; S \in_{\mathcal{P}X} \mathcal{C}\;\Rightarrow\; S \cup_X \{a\}_X \in_{\mathcal{P}X} \mathcal{C}) \;\Rightarrow\; \forall\,S\colon \mathcal{P}X,\; S \in_{\mathcal{P}X} \mathcal{C} \text{.}$$
This does induction over subsets of an arbitrary set $X$ rather than over sets themselves.  (Thanks to Ingo Blechschmidt for reminding me that this can be done!)  Actually, the clause $\neg\, (a \in_X S)$ can be omitted, giving an a priori weaker axiom (Kuratowski finiteness), which is equivalent in a boolean topos.
The axiom scheme proves the above axiom, but I haven't gone through all of the sentences of $\operatorname{ETCS}$ to see if the axiom proves each instance of the axiom scheme.  (Offhand, I'd guess not.)
