Underlying language to specify various types of logic
One answer is that we use English, but that's not what you're looking for.

To make the question more precise, let us ask what sort of formalism is useful for describing logics. This is still quite broad, because a logic has several parts: syntax, rules of inference, semantics, etc.

Syntax is pretty well understood and we know that the syntax of a language can be described in terms of formal grammar. That is a well developed theory. In any case, concrete syntax is rather boring from the point of view of logic.

It is far more interesting to ask what we need to specify the inference rules for a logic. Because a general logic can be just about any formal system, let us consider only traditional logics: classical first-order, intuitionistic first-order, second order, higher-order, simple type theory, dependent type theory and so on. One answer is that we should use a logical framework (LF). It is a variant of type theory designed in such a way that when we specify a logic in it we have:


  A statement in the logic is provable if, and only if, the corresponding type in the logical framework is inhabited.


This is desirable because it says that the logical framework is neither too weak nor too powerful.

In terms of logical strength LF is very weak: it is a dependent type theory with first-order kinds and $\Pi$'s. Speaking vaguely and in terms of logical connectives, this is a bit like using as our meta-theory a logic which has only $\forall$ and $\Rightarrow$ (and no equality).

There are implementations of logical frameworks, for instance Twelf. Of course, the point of such a tool is not just description of logics, but also the study of their meta-theoretic properties. Among the Twelf case studies you can find formalization in LF of cut elimination, the double negation translation, classical modal logic S5, and a bunch of more programming-language oriented examples.

One may also ask what formalism is necessary to specify semantics of a logic. The semantics of traditional classical first-order logic goes under the name of Tarski model theory and uses set theory, although it is well known that a much weaker system suffices (a fragment of Peano arithmetic). Other kinds of logic require different approaches, but in general it is the case that the meta-theory needed for the description of semantics is much less complicated than the semantics itself. For instance, the models of intuitionistic higher-order logic are elementary toposes. The axioms for an elementary topos are essentially algebraic, i.e., we can express all the axioms of an elementary topos with equations (we do not even need any logical connectives, just equations), see Section II.2 of Lambek and Scott's "Introduction to Higher-Order Categorical Logic".