a) side effects are "masked" in Haskell in that a function that is generic over any type of monad may or may not incur side effects at run-time, depending on which actual monad it is used with.
b) see above - because monads as a type class exist, a function may be written with a type signature that does not indicate in any way that it will be eventually used over IO.
c) the fact that the Haskell denotational semantics are entirely silent over what happens at run-time with the IO monad is definitely a loophole. From a birds view, a Haskell program is a giant expression that reduces to an object of type IO, and what happens with that object is entirely outside of the language semantics.
a-b) The objects of type IO are values, just as any other monad. It is true that polymorphic functions can be instantiated with type IO, just as they can be of any other type. How you think this supports the assertion that side-effects are "masked" is beyond me.
c) The language boundary of Haskell typically ends at the production of an IO value. You can easily give an operational semantics to many IO operations, and in fact there are papers that do this for simple IO operations such as putStr. It's not possible to give a full operational semantics for IO in any language, not just Haskell. Of course you are going to model console I/O, references, exceptions, concurrency features (all of which have been done). But these aren't the only kinds of side effects. Does your model account for the network, and all its complexities? Does your model account for power failures? Does your model account for cosmic rays? Most models don't, but nobody calls them loopholes, nobody implies it's a big cover-up. Every model is going to have a boundary, and Haskell's seems good enough to me. It's no more undefined than, say, ML.
a and b don't actually matter, because what matters is how the function is called. If given some `f :: Monad m => m -> m`, then you can only call f with IO as the monad from an already impure context. For example, you can't call f with IO from inside a function (g :: a -> b).
The purpose of IO in Haskell is to explicitly mark side effects, because they cannot be arbitrarily composed in the way pure functions can. IO represents a one-way boundary in that you can turn some pure computation into an impure one (a -> IO a), but there is no way of "extracting" that computation back from IO (i.e, there exist no (IO a -> a)). That "monads" are used to do this is useful because they provide the (a -> IO a), and happen to have a convenient function for chaining computations (IO a -> (a -> IO b) -> IO b).
How IO is defined is up to the implementation, and not in the scope of the language - different implementations could use a different representation for IO - what matters is that it must be defined in a way that one cannot define an (IO a -> a).
On "a Haskell program is a giant expression that reduces to an object of type IO", this is really nothing to do with Haskell, but a consequence of how we've built our operating systems and how the defacto meaning of "program" these days is equivalent to an "executable file". Traditionally "program" was much more abstract and could refer simply to any piece of code, such as a (pure) haskell function. We can consider any Haskell function to be a "program" in itself. If we had an environment from which we launched processes which provided all the command line switches and environment variables as arguments, we could easily omit the "IO" from our "main", if the rest of our code was pure. (On a side note, this is precisely what early versions of Haskell did, before monadic IO became practical)
b) see above - because monads as a type class exist, a function may be written with a type signature that does not indicate in any way that it will be eventually used over IO.
c) the fact that the Haskell denotational semantics are entirely silent over what happens at run-time with the IO monad is definitely a loophole. From a birds view, a Haskell program is a giant expression that reduces to an object of type IO, and what happens with that object is entirely outside of the language semantics.