Occasionally I come across a definition based on what will happen in all models, for example, that a contradiction is a statement that is false in all models, that a tautology is a statement that is true in all models, that sentence A implies sentence B if in all models in which A is true, B is also true, and similar for "and" and "or". But these definitions cannot be formalized as is, because they quantify over "all models", an impossibility. How does one get around this? Does one quantify over all models of first-order theories inside a second-order theory?
You would need to specify your meta-system, before you can formalize a meta-theoretic statement. Conventionally logicians use some conservative extension of ZFC as their meta-system. Within ZFC one can consider any first-order language and collection of sentences (encoded in some way) over it, and ask whether there is a model, which is defined as a tuple consisting of a set for the domain and interpretations for each predicate or function or constant symbol of the language.
However, this definition does not give a set of all models, because no such set can exist (unless you love contradictions). But "$M$ is a model of $X$" can be expressed by a first-order sentence over ZFC. So what you can do is to define a new abbreviation $IsModelOf$, namely a binary predicate symbol such that, for every (sets) $M,X$, we have $IsModelOf(M,X)$ iff $M$ is a model of $X$.
Quantifying over all models is then possible, since restricted quantification over elements satisfying a predicate can be easily expressed using unrestricted quantification. What cannot be done is to use the collection of all models as a single object in the set-theoretic universe. You are right that if you use second order ZFC you can natively have the collection of all (set) models of a set of sentences. One commonly used essentially second-order set theory is MK (Morse-Kelley), which has two sorts, one for sets and one for collections of sets called classes.