How is pre-image resistance defined, formally? Earlier today, forest asked in our chat, The Side Channel whether the definition of first pre-image security actually requires that an input that evaluates to the challenge hash result must be known to exist a-priori.

This got me thinking. How does one actually, formally define first pre-image security for hash functions?

This is also motivated by the fact that formal definitions are crucial in cryptography to actually understand what is needed to break security. For example, the RSA problem isn't "given $c$ that was constructed as $c=m^e\bmod n$, find $m$" but rather requires specific properties from $n$ (by requiring correct key generation) and requires correct choice (uniformly at random) of $m$ as well.
$\newcommand{\xs}{\xleftarrow\$}\newcommand{\mc}{\mathcal}$
There is a paper from 2004 (last revised 2009) by Rogaway and Shrimpton "Cryptographic Hash-Function Basics: Definitions, Implications and Separations for Preimage Resistance, Second-Preimage Resistance, and Collision Resistance" which talks about this very topic (among others). I shall use it as the primary reference of this answer.

In the paper, there are three definitions given for first pre-image resistance. One which is separate from the others, one somewhat weaker and a strong one (to which quite a few other properties also reduce to). So we shall go through them in order.

Before we can start though, we need to take a moment to acustom to the fact that any hash function is written as $H_K(M)$ from here on, i.e. that the hash functions take a "key" as well. This is done to be able to model them as random functions and in practice this "key" can be assumed to be fixed and e.g. represent the initial internal chaining value of the hash function or a salt-like input to the hash. So from here on, let our hash function be $H:\mathcal K\times \mathcal M\to\mathcal Y$ and let $m$ be an integer such that $\{0,1\}^m\subseteq\mathcal M$, i.e. pick a length $m$ of bit strings that is a valid input length to the hash function. This set is useful because it allows us to reason about a finite subset of the potentially infinitely large hash input and we can make any choice of $m$ to our liking to model a particular string length.

Also all the definitions will talk about advantages for some adversary and some auxilliary parameters. Usually you want to bound this advantage to be negligble (in some security parameter, e.g. the digest length or the input entropy) for all adversaries that run in polynomial cost (i.e. efficiently and don't just enumerate the hash) and for all auxiliary parameters.

Definition 1: everywhere Preimage resistance (ePre)

$$\mathrm{Adv}^{\text{ePre}}_H(A)=\max_{Y\in\mc Y}\{\Pr[K\xs\mc K;M\xs A(K):H_K(M)=Y]\}$$

So what does this definition say? First, iterate over all possible output values $Y$. Next pick a hash function uniformly the selection. Then ask the attacker to come up with a value given the function selection. The attacker "wins" for the given $Y$ value if they actually found a pre-image. Now take the advantage of the attacker to be the maximum over all possible choices of $Y$.

Now this definition essentially says that it should be hard for an attacker to come up with a pre-image for any output value, given that they had no a-priori knowledge of the concrete (secure) variation of the hash. 

It may appear that this definition isn't all that useful in practice, because an attacker may just always guess the empty string, but as the range point is fixed first and then the hash is selected uniformly at random, there's a $1/|\mc K|$ probability of being right with the guess, which is negligible. Thanks to Maeher for pointing this error out in a previous version of this answer.

Definition 2: always Preimage resistance (aPre)

$$\mathrm{Adv}_H^{\text{aPre}[m]}(A)=\max_{K\in \mc K}\{\Pr[M\xs\{0,1\}^m;Y\gets H_K(M);M'\xs A(Y):H_K(M')=Y]\}$$

What does this mean? Well, first it asks to iterate over all possible hash selections and fix one, e.g. the concrete instance. Now pick a message uniformly at random. Hash it using the hash instance. Hand the result to the adversary and ask them to come up with a value. If this value is actually a pre-image of the value given hash function then the adversary won. 

Now practically speaking it appears that this definition is the one most closely modeling actual hash functions, because you fix the selection of the function and then ask the adversay to find a pre-image for a randomly chosen message.

Definition 3: Preimage resistance (Pre)

$$\mathrm{Adv}_H^{\text{Pre}[m]}(A)=\Pr[K\xs\mc K;M\xs\mc \{0,1\}^m;Y\gets H_K(M);M'\xs A(K,Y):H_K(M')=Y]$$

So what does this mean? Well it first says that you should pick an instance of the hash function uniformly at random. Then we pick a message uniformly at random from the set of bit strings of length $m$. Next we compute the challenge output value $Y$ using the previously determined message and function selection. Finally we give the adversary, ie the attacker both our function selection and the output value and ask it to come up with a value. If that value is indeed a first-preimage then the attacker "won". The advantage an attacker has now is the probability over the choice of the function selection and the value selection that they can come up with a valid pre-image.